A COMPARATIVE STUDY OF SEVERAL PROOF PROCEDURESBIBEL W.1982; ARTIFICIAL INTELLIGENCE; ISSN 0374-2539; NLD; DA. 1982; VOL. 18; NO 3; PP. 269-293; BIBL. 21 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

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

A UNIFICATION ALGORITHM FOR ASSOCIATIVE-COMMUTATIVE FUNCTIONSSTICKEL ME.1981; J. ASSOC. COMPUT. MACH.; ISSN 0004-5411; USA; DA. 1981; VOL. 28; NO 3; PP. 423-434; BIBL. 17 REF.Article

VARIABLE ELIMINATION AND CHAINING IN A RESOLUTION-BASED PROVER FOR INEQUALITIESBLEDSOE WW; HINES LM.1980; LECTURE NOTES COMPUTER SCI.; DEU; DA. 1980; VOL. 87; PP. 70-87; BIBL. 11 REF.Conference Paper

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

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

PROOF BY MATRIX REDUCTION AS PLAN+VALIDATIONCAFERRA R.1982; LECTURE NOTES IN COMPUTER SCIENCE; ISSN 0302-9743; DEU; DA. 1982; VOL. 138; PP. 309-325; BIBL. 26 REF.Conference Paper

THEOREM PROVING WITH ABSTRACTIONPLAISTED DA.1981; ARTIF. INTELL.; ISSN 0374-2539; NLD; DA. 1981; VOL. 16; NO 1; PP. 47-108; BIBL. 15 REF.Article

HYPERPARAMODULATION: A REFINEMENT OF PARAMODULATIONWOS L; OVERBEEK R; HENSCHEN L et al.1980; LECTURE NOTES COMPUTER SCI.; DEU; DA. 1980; VOL. 87; PP. 208-219; BIBL. 7 REF.Conference Paper

THE INTERACTION OF OBSERVATION AND INFERENCE IN A FORMAL REPRESENTATION SYSTEMFILMAN RE.1979; IJCAI 79. INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE. 6/1979/TOKYO; USA; S.1.: INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE; DA. 1979; VOL. 1; PP. 269-274; BIBL. 10 REF.Conference Paper

A PROVER FOR GENERAL INEQUALITIESBLEDSDOE WW; BRUELL P; SHOSTAK R et al.1979; IJCAI 79. INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE. 6/1979/TOKYO; USA; S.1.: INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE; DA. 1979; VOL. 1; PP. 66-69; BIBL. 10 REF.Conference Paper

CASC-J3 the 3rd IJCAR ATP system competitionSUTCLIFFE, Geoff.Lecture notes in computer science. 2006, pp 572-573, issn 0302-9743, isbn 3-540-37187-7, 1Vol, 2 p.Conference Paper

Automated deduction - CADE-19 (Miami Beach FL, 28 July - 2 August 2003)Baader, Franz.Lecture notes in computer science. 2003, issn 0302-9743, isbn 3-540-40559-3, XII, 502 p, isbn 3-540-40559-3Conference Proceedings

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

INTUITIONISTIC BASIS FOR NON-MONOTONIC LOGICGABBAY DM.1982; LECTURE NOTES IN COMPUTER SCIENCE; ISSN 0302-9743; DEU; DA. 1982; VOL. 138; PP. 260-273; BIBL. 5 REF.Conference Paper

CALCULS POUR LES DEMONSTRATIONS ASSISTEES PAR ORDINATEUR ET RESULTATS DE LEUR APPLICATION DANS DIFFERENTES BRANCHES DES MATHEMATIQUESPANKOV PS; BAYACHOROVA DB; YUGAJ SA et al.1982; KIBERNETIKA; ISSN 506850; UKR; DA. 1982; NO 6; PP. 111-116; BIBL. 18 REF.Article

PRINCIPES DE PLANIFICATION DE LA RESOLUTION DES PROBLEMES DANS UN SYSTEME DE SYNTHESE AUTOMATIQUE DES PROGRAMMESLAVROV SS; ZALOGOVA LA; PETRUSHINA TI et al.1982; PROGRAMMIROVANIE; ISSN 508098; SUN; DA. 1982; NO 3; PP. 35-43; BIBL. 3 REF.Article

QUATRE ALGORITHMES RAPIDES DANS LA METHODE DES RESOLUTIONSKOSSEJ IP.1982; IZVESTIJA AKEDEMII NAUK SSSR. TEHNICESKAJA KIBERNETIKA; ISSN 0002-3388; SUN; DA. 1982; NO 5; PP. 217-221; BIBL. 4 REF.Article

A SYSTEM FOR PROVING EQUIVALENCES OF RECURSIVE PROGRAMSKOTT L.1980; LECTURE NOTES COMPUTER SCI.; DEU; DA. 1980; VOL. 87; PP. 63-69; BIBL. 17 REF.Conference Paper

ANALYST - UN PAQUET DE PROGRAMMES POUR LA DEMONSTRATION DES IDENTITES (THEOREMES) DANS LES SYSTEMES D'ALGEBRES ALGORITHMIQUES AXIOMATISESKIRSANOV GM; TSEJTLIN GE; YUSHCHENKO EL et al.1979; KIBERNETIKA; UKR; DA. 1979; NO 4; PP. 28-33; ABS. ENG; BIBL. 12 REF.Article

A MECHANICAL PROOF OF TERMINATION OF TAKEUCHI'S FUNCTIONMOORE JS.1979; INFORM. PROCESSG LETTERS; NLD; DA. 1979; VOL. 9; NO 4; PP. 176-181; BIBL. 7 REF.Article

AUTOMATIC DEDUCTION AND EQUALITYDIGRICOLI VJ.1979; ACM 79. ASSOCIATION FOR COMPUTING MACHINERY. 1979 ANNUAL CONFERENCE/1979/DETROIT MI; USA; NEW YORK: ACM; DA. 1979; PP. 240-250; BIBL. 13 REF.Conference Paper

AUTOMATED THEOREM PROVING: A LOGICAL BASISLOVELAND DW.1978; FUNDAM. STUD. COMPUTER SCI.; NLD; DA. 1978; VOL. 6; 417 P.; BIBL. 5 P.Serial Issue

UN PROGRAMME DE DEMONSTRATION AUTOMATIQUE D'EXERCIES D'ARITHMETIQUE.BOURGOIN D.1977; IN: CONGR. INT. CYBERN. 8. ACTES; NAMUR; 1976; NAMUR; ASSOC. INT. CYBERN.; DA. 1977; PP. 359-366; BIBL. 6 REF.Conference Paper