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

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

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

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

RESOLUTION, REFINEMENTS, AND SEARCH STRATEGIES: A COMPARATIVE STUDY.WILSON GA; MINKER J.1976; I.E.E.E. TRANS. COMPUTERS; U.S.A.; DA. 1976; VOL. 25; NO 8; PP. 782-801; BIBL. 42 REF.Article

DEMONSTRATION AUTOMATIQUE DE THEOREMES EN THEORIE DES ENSEMBLES.PASTRE D.1976; ; S.L.; DA. 1976; PP. 1-151; BIBL. 2 P. 1/2; (THESE DOCT. 3E. CYCLE, SPEC. MATH. APPL., MENTION INF.; PIERRE ET MARIE CURIE PARIS 6)Thesis

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

SUR LES METHODES DE PRESCRIPTION ET DE CONSTRUCTION PARTIELLE D'UNE THEORIE SUR UN CALCULATEURMART'YANOV VI.1982; KIBERNETIKA; ISSN 506850; UKR; DA. 1982; NO 6; PP. 102-110; BIBL. 18 REF.Article

USING SOPHISTICATED MODELS IN RESOLUTION THEOREM PROVINGSANDFORD DAVID M.1980; LECTURE NOTES COMPUTER SCI.; DEU; DA. 1980; NO 90; XI-239 P.; BIBL. 37 REF.Serial Issue

A NEW METHOD FOR PROVING CERTAIN PRESBURGER FORMULAS.BLEDSOE WW.1975; IN: INT. JOINT CONF. ARTIF. INTELL. 4. ADV. PAP.; TBILISI; 1975; CAMBRIDGE, MASS.; ARTIF. INTELL. LAB.; DA. 1975; VOL. 1; PP. 15-21; BIBL. 11 REF.Conference Paper

AUTOMATED HYPOTHESIS GENERATION USING EXTENDED INDUCTIVE RESOLUTION.MORGAN CG.1975; IN: INST. JOINT CONF. ARTIF. INTELL. 4. ADV. PAP; TBILISI; 1975; CAMBRIDGE, MASS.; ARTIF. INTELL. LAB.; DA. 1975; VOL. 1; PP. 351-356; BIBL. 13 REF.Conference Paper