AN EXTENSION OF UNIFICATION TO SUBSTITUTIONS WITH AN APPLICATION TO AUTOMATIC THEOREM PROVING.VAN VAALEN J.1974; STICHTG MATH. CENTRUM, INFORMAT.; NEDERL.; DA. 1974; NO 24; PP. 1-20; BIBL. 6 REF.Article

COMPUTER PROOFS OF LIMIT THEOREMS.BLEDSOE WW; BOYER RS; HENNEMAN WH et al.1972; ARTIF. INTELLIG.; U.S.A.; DA. 1972; VOL. 3; PP. 27-60; BIBL. 7 REF.Article

THEOREM-PROVING SYSTEMSORLOWSKA E.1973; DISSERT. MATH.; POLOGNE; DA. 1973; VOL. 103; PP. 1-55; BIBL. 3 P. 1/2Serial Issue

BERNOULLI AND THE PAPER DIRIGIBLE.EDGE RD.1976; AMER. J. PHYS.; U.S.A.; DA. 1976; VOL. 44; NO 8; PP. 780-781; BIBL. 1 REF.Article

LOGIC MACHINE ARCHITECTURE: KERNEL FUNCTIONSLUSK EL; MCCUNE WW; OVERBEEK RA et al.1982; LECTURE NOTES IN COMPUTER SCIENCE; ISSN 0302-9743; DEU; DA. 1982; VOL. 138; PP. 70-84; BIBL. 8 REF.Conference Paper

A SIMPLE DEDUCTION METHOD FOR MODAL LOGICFARINAS DEL CERRO L.1982; INF. PROCESS. LETT.; ISSN 0020-0190; NLD; DA. 1982; VOL. 14; NO 2; PP. 49-51; BIBL. 8 REF.Article

ON THE ROLE OF UNIFICATION IN MECHANICAL THEOREM PROVING.SHOSTAK RE.1977; ACTA INFORMAT.; ALLEM.; DA. 1977; VOL. 7; NO 3; PP. 319-323; BIBL. 8 REF.Article

CONVERSION OF PREDICATE-CALCULUS AXIOMS TO CORRESPONDING DETERMINISTIC PROGRAMS.SANDEWALL E.1976; I.E.E.E. TRANS. COMPUTERS; U.S.A.; DA. 1976; VOL. 25; NO 4; PP. 342-346; BIBL. 14 REF.; (INT. JT. CONF. ARTIF. INTELL. 3; STANFORD, CALIF.; 1973)Conference Paper

ON A NEW PROOF OF MOSER'S TWIST MAPPING THEOREM.RUSSMANN H.1976; CELEST. MECH.; NETHERL.; DA. 1976; VOL. 14; NO 1; PP. 19-31; BIBL. 4 REF.; (CONF. MATH. METHODS CELESTIAL MECH. 5. PROC.; OBERWOLFACH; 1975)Conference Paper

PLANE GEOMETRY THEOREM PROVING USING FORWARD CHAINING.NEVINS AJ.1975; ARTIF. INTELLIG.; U.S.A.; DA. 1975; VOL. 6; NO 1; PP. 1-23; BIBL. 14 REF.Article

PROVING THEOREMS ABOUT LISP FUNCTIONS.BOYER RS; MOORE JS.1975; J. ASS. COMPUTG MACHIN.; U.S.A.; DA. 1975; VOL. 22; NO 1; PP. 129-144; BIBL. 27 REF.Article

A PROBABILISTIC APPROACH TO AUTOMATON-ENVIRONMENT SYSTEMS.KRAMOSIL I.1975; KYVERNETIKA; CESKOSL.; DA. 1975; VOL. 11; NO 3; PP. 173-206; BIBL. 14 REF.Article

A PROOF PROCEDURE USING CONNECTION GRAPHS.KOWALSKI R.1975; J. ASS. COMPUTG MACHIN.; U.S.A.; DA. 1975; VOL. 22; NO 4; PP. 572-595; BIBL. 1 P. 1/2Article

COMPLEXITY OF THEOREM-PROVING PROCEDURES: SOME GENERAL PROPERTIES.LONGO G; VENTURINI ZILLI M.1974; REV. FR. AUTOMAT. INFORMAT. RECH. OPERAT., R; FR.; DA. 1974; VOL. 8; NO 3; PP. 5-18; BIBL. 11 REF.Article

STATISTICAL METHODS FOR COMPARING THEOREM PROVING ALGORITHMS. = METHODES STATISTIQUES DE COMPARAISON D'ALGORITHMES DE DEMONSTRATION AUTOMATIQUE DE THEOREMESKRAMOSIL I; ZWINOGRODZKI Z.1974; KYBERNETIKA; CESKOSL.; DA. 1974; VOL. 10; NO 3; PP. 221-240; BIBL. 1 P. 1/2Article

THE EARLEY ALGORITHM AS A PROBLEM REPRESENTATION.MINKER J; VANDERBRUG GJ.1974; INFORM. PROCESSG LETTERS; NETHERL.; DA. 1974; VOL. 3; NO 1; PP. 1-7; BIBL. 9 REF.Article

ON MAKING A THEOREM FOR A CHILD = SUR LA CONCEPTION D'UN THEOREME POUR UN ENFANTPAPERT S.1972; IN: ASSOC. COMPUT. MACH. ANN. CONF. PROC. BOSTON, 1972; NEW YORK; ASSOC. COMPUT. MACH.; DA. 1972; VOL. 1; PP. 345-349Conference Proceedings

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

NEW VERSIONS OF THE LINDEBERG-FELLER THEOREMJESIAK B; ROSSBERG HJ.1981; TEOR. VEROJATN. EE PRIMEN.; ISSN 0040-361X; SUN; DA. 1981; VOL. 26; NO 4; PP. 858-862; ABS. RUS; BIBL. 7 REF.Article

A RESOLUTION-BASED PROOF PROCEDURE USING DELETION-DIRECTED SEARCH.GELPERIN D.1976; I.E.E.E. TRANS. COMPUTERS; U.S.A.; DA. 1976; VOL. 25; NO 4; PP. 323-327; BIBL. 16 REF.; (INT. JT. CONF. ARTIF. INTELL. 3; STANFORD, CALIF.; 1973)Conference Paper

A SEMANTICALLY GUIDED DEDUCTIVE SYSTEM FOR AUTOMATIC THEOREM PROVING.REITER R.1976; I.E.E.E. TRANS. COMPUTERS; U.S.A.; DA. 1976; VOL. 25; NO 4; PP. 328-334; BIBL. 14 REF.; (INT. JT. CONF. ARTIF. INTELL. 3; STANFORD, CALIF.; 1973)Conference Paper

REASONING ABOUT PROGRAMS.WALDINGER RJ; LEVITT KN.1974; ARTIF. INTELLIG.; U.S.A.; DA. 1974; VOL. 5; NO 3; PP. 235-316; BIBL. 1 P. 1/2Article

AUTOMATED THEOREM-PROVING FOR THEORIES WITH SIMPLIFIERS, COMMUTATIVITY, AND ASSOCIATIVITY.SLAGLE JR.1974; J. ASS. COMPUTG MACHIN.; U.S.A.; DA. 1974; VOL. 21; NO 4; PP. 622-642; BIBL. 15 REF.Article

AUTOMATISATION DE LA RECHERCHE DES DEMONSTRATIONS DE THEOREMES DE MATHEMATIQUES ET MACHINES D'INTELLIGENCE ARTIFICIELLEGLUSHKOV VM; KAPITONOVA YU V.1972; KIBERNETIKA, U.S.S.R.; S.S.S.R.; DA. 1972; NO 5; PP. 2-6; BIBL. 8 REF.Serial Issue

COMPARISON OF NATURAL DEDUCTION AND LOCKING RESOLUTION IMPLEMENTATIONSGREENBAUM S; NAGASAKA A; O'RORKE P et al.1982; LECTURE NOTES IN COMPUTER SCIENCE; ISSN 0302-9743; DEU; DA. 1982; VOL. 138; PP. 159-171; BIBL. 16 REF.Conference Paper