A case study in automated theorem proving: Finding sages in combinatory logic William McCuneLarry Wos Problem Corner Pages: 91 - 107
Some obstacles to the automation of reasoning, and the problem of redundant information Larry Wos Basic Research Problem Pages: 81 - 90
A class of confluent term rewriting systems and unification Jia-Huai YouP. A. Subrahmanyam OriginalPaper Pages: 391 - 418
Automated reasoning in geometry theorem proving with Prolog Helder CoelhoLuis Moniz Pereira OriginalPaper Pages: 329 - 390
Set theory in first-order logic: Clauses for Gödel's axioms Robert BoyerEwing LuskLawrence Wos Problem Corner Pages: 287 - 327
The theory of idempotent semigroups is of unification type zero Franz Baader OriginalPaper Pages: 283 - 286
Unification under associativity and idempotence is of type nullary Manfred Schmidt-Schauss OriginalPaper Pages: 277 - 281
Proving geometry theorems with rewrite rules Shang-Ching ChouWilliam F. Schelter OriginalPaper Pages: 253 - 273
Basic principles of mechanical theorem proving in elementary geometries Wu Wen-Tsun OriginalPaper Pages: 221 - 252
Editor's preface to ‘basic principles of mechanical theorem proving in elementary geometries’ by Wu Wen-tsun J Strother Moore EditorialNotes Pages: 219 - 220
Seventy-five problems for testing automatic theorem provers Francis Jeffry Pelletier Problem Corner Pages: 191 - 216
A decision procedure for combinations of propositional temporal logic and other specialized theories David A. Plaisted OriginalPaper Pages: 171 - 190
Negation as Failure. Completeness of the Query Evaluation Process for horn clause programs with recursive definitions C. AquilanoR. BarbutiM. Martelli OriginalPaper Pages: 155 - 170
Automated analysis of operators on state tables: A technique for intelligent search Thomas Kramer OriginalPaper Pages: 127 - 153
Correctness criteria of some algorithms for uncertain reasoning using Incidence Calculus Alan Bundy OriginalPaper Pages: 109 - 126
Schubert's Steamroller problem: Formulations and solutions Mark E. Stickel Problem Corner Pages: 89 - 101
Proving termination of normalization functions for conditional expressions Lawrence C. Paulson OriginalPaper Pages: 63 - 74
Intelligent backtracking in deduction systems by means of extended unification graphs Werner DilgerAgnes Janson OriginalPaper Pages: 43 - 62
Job-shop scheduling using automated reasoning: A case study of the car-sequencing problem Bruce D. ParrelloWaldo C. KabatL. Wos OriginalPaper Pages: 1 - 42
Writing programs that construct proofs R. L. ConstableT. B. KnoblockJ. L. Bates OriginalPaper Pages: 285 - 326
Incidence calculus: A mechanism for probabilistic reasoning Alan Bundy OriginalPaper Pages: 263 - 283
Experiments with semantic paramodulation William McCuneLawrence Henschen OriginalPaper Pages: 231 - 261
The concept and implementation of skeletal plans Peter E. FriedlandYumi Iwasaki OriginalPaper Pages: 161 - 208
An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem David M. Russinoff OriginalPaper Pages: 121 - 139
On the role of automated theorem proving in the compile-time derivation of concurrency Christian Lengauer OriginalPaper Pages: 75 - 101
ROGET: A knowledge-based system for acquiring the conceptual structure of a diagnostic expert system James S. Bennett OriginalPaper Pages: 49 - 74