INTRODUCING ITERATION INTO THE PURE LISP THEOREM PROVER.MOORE JS.1975; I.E.E.E. TRANS. SOFTWARE ENGNG; U.S.A.; DA. 1975; VOL. 1; NO 3; PP. 328-338; BIBL. 10 REF.Article

REVUE ET BIBLIOGRAPHIE DES TRAVAUX SUR L'AUTOMATISATION DE LA RECHERCHE DES DEMONSTRATIONS DE THEOREMES DANS LES THEORIES FORMELLESKAPITONOVA YU V; KOSTYRKO VF; LYALETSKIJ AV et al.1972; KIBERNETIKA, U.S.S.R.; S.S.S.R.; DA. 1972; NO 5; PP. 7-18; BIBL. 8 P.Serial Issue

LA RECHERCHE DE LA DEDUCTION CONSIDEREE COMME UN MODELE DE PROCESSUS HEURISTIQUEMASLOV S YU.1972; KIBERNETIKA, U.S.S.R.; S.S.S.R.; DA. 1972; NO 5; PP. 74-78; BIBL. 26 REF.Serial Issue

SEMIGROUPS, ANTIAUTOMORPHISMS, AND INVOLUTIONS: A COMPUTER SOLUTION TO AN OPEN PROBLEM. IWINKER SK; WOS L; LUSK EL et al.1981; MATH. COMPUT.; ISSN 0025-5718; USA; DA. 1981; VOL. 37; NO 156; PP. 533-545; BIBL. 6 REF.Article

AN INVESTIGATION INTO THE GOALS OF RESEARCH IN AUTOMATIC THEOREM PROVING AS RELATED TO MATHEMATICAL REASONINGBROWN FM.1980; ARTIF. INTELL.; ISSN 0374-2539; NLD; DA. 1980; VOL. 14; NO 3; PP. 221-242; BIBL. 7 REF.Article

ALGORITHME ET EXPERIENCE DE RECHERCHE DES DEMONSTRATIONS DE THEOREMES DANS LE CALCUL PROPOSITIONNELANUFRIEV FV; KOSTYAKOV VM; MALASHONOK AI et al.1972; KIBERNETIKA, U.S.S.R.; S.S.S.R.; DA. 1972; NO 5; PP. 68-73; BIBL. 4 REF.Serial Issue

TRANSFORMING MATINGS INTO NATURAL DEDUCTION PROOFSANDREWS PB.1980; LECTURE NOTES COMPUTER SCI.; DEU; DA. 1980; VOL. 87; PP. 281-292; BIBL. 9 REF.Conference Paper

PROVING THEOREMS WITH THE MODIFICATION METHOD.BRAND D.1975; S.I.A.M. J. COMPUTG; U.S.A.; DA. 1975; VOL. 4; NO 4; PP. 412-430; BIBL. 10 REF.Article

THE LINKED CONJUNCT METHOD FOR AUTOMATIC DEDUCTION AND RELATED SEARCH TECHNIQUESOMODEO EG.1982; COMPUT. MATH. WITH APPL.; ISSN 0097-4943; USA; DA. 1982; VOL. 8; NO 3; PP. 185-203; BIBL. 31 REF.Article

ON AN IF-THEN-ELSE TECHNIQUE FOR AUTOMATED THEOREM PROVING IN PROPOSITIONAL CALCULUSDABIJA V.1981; BULL. INST. POLITEH. "GHEORGHE GHEORGHIU-DEJ" BUCURESTI, ELECTROTEH.; ROM; DA. 1981; VOL. 48; NO 2; PP. 95-100; ABS. RUM; BIBL. 4 REF.Article

EXPONENTIAL IMPROVEMENT OF EFFICIENT BACKTRACKING: A STRATEGY FOR PLAN-BASED DEDUCTIONPIETRZYKOWSKI T; MATWIN S.1982; LECTURE NOTES IN COMPUTER SCIENCE; ISSN 0302-9743; DEU; DA. 1982; VOL. 138; PP. 223-239; BIBL. 15 REF.Conference Paper

DELETING REPEATED GOALS IN THE PROBLEM REDUCTION FORMATLOUELAND DW; REDDY CR.1981; J. ASSOC. COMPUT. MACH.; ISSN 0004-5411; USA; DA. 1981; VOL. 28; NO 4; PP. 646-661; BIBL. 14 REF.Article

THEOREM PROVING VIA GENERAL MATINGSANDREWS PB.1981; J. ASSOC. COMPUT. MACH.; ISSN 0004-5411; USA; DA. 1981; VOL. 28; NO 2; PP. 193-214; BIBL. 31 REF.Article

Termination of {aa → bc, bb → ac, cc → ab}HOFBAUER, Dieter; WALDMANN, Johannes.Information processing letters. 2006, Vol 98, Num 4, pp 156-158, issn 0020-0190, 3 p.Article

The Homer systemCOLTON, Simon; HUCZYNSKA, Sophie.Lecture notes in computer science. 2003, pp 289-294, issn 0302-9743, isbn 3-540-40559-3, 6 p.Conference Paper

Completeness results of inequality proversBLEDSOE, W. W; KUNEN, K; SHOSTAK, R et al.Artificial intelligence. 1985, Vol 27, Num 3, pp 255-288, issn 0004-3702Article

EXPERIMENTS WITH RESOLUTION-BASED THEOREM-PROVING ALGORITHMSLUSK EL; OVERBEEK RA.1982; COMPUT. MATH. WITH APPL.; ISSN 0097-4943; USA; DA. 1982; VOL. 8; NO 2; PP. 141-152; BIBL. 7 REF.Article

PROCEDURE IMPLEMENTATION THROUGH DEMODULATION AND RELATED TRICKSWINKER SK; WOS L.1982; LECTURE NOTES IN COMPUTER SCIENCE; ISSN 0302-9743; DEU; DA. 1982; VOL. 138; PP. 109-131; BIBL. 26 REF.Conference Paper

DEMONSTRATION AUTOMATIQUE: REFUTATION PAR SUPERPOSITION DE CLAUSES EQUATIONNELLES = AUTOMATIC PROOF: REFUTATION BY SUPERPOSITION OF EQUATIONAL CLAUSESFRIBOURG LAURENT.1982; ; FRA; DA. 1982; 145 F.; 30 CM; BIBL. 3 P.; TH. 3E CYCLE: MATH./PARIS 7/1982Thesis

A LOOK AT TPSMILLER DA; COHEN E; ANDREWS PB et al.1982; LECTURE NOTES IN COMPUTER SCIENCE; ISSN 0302-9743; DEU; DA. 1982; VOL. 138; PP. 50-69; BIBL. 7 REF.Conference Paper

EFFICIENT RESOLUTION THEOREM PROVING IN THE PROPOSITIONAL LOGICFIBY R; SOKOL J; SUDOLSKY M et al.1979; C. L. AND C. L.; HUN; DA. 1979; VOL. 13; PP. 151-168; BIBL. 40 REF.Article

DOING ARITHMETIC WITH RESOLUTIONSTEDRON B.1978; SCRIPTA FAC. SCI. NAT. UNIV. PURKYN. BRUN.; CSK; DA. 1978; VOL. 8; NO 10; PP. 63-67; BIBL. 7 REF.Article

PRINCIPE DE COMPARAISON POUR LA DEMONSTRATION AUTOMATIQUE DE THEOREMES. IMATROSOV VM; VASIL'EV SN.1978; IZVEST. AKAD. NAUK S.S.S.R., TEKH. KIBERN.; S.S.S.R.; DA. 1978; NO 2; PP. 60-69; BIBL. 20 REF.Article

PROBLEMS AND EXPERIMENTS FOR AND WITH AUTOMATED THEOREM-PROVING PROGRAMS.MCCHAREN JD; OVERBEEK RA; WOS LA et al.1976; I.E.E.E. TRANS. COMPUTERS; U.S.A.; DA. 1976; VOL. 25; NO 8; PP. 773-782; BIBL. 5 REF.Article

Les modèles analogiques et le contrôle dans les systèmes à base de règles = Analogical models and the control in rule-based systemsPloux, Sabine; Fouet, Jean-Marc.1992, 155 p.Thesis