-
1
-
First-order theorem proving using conditional rewrite rules
-
21
-
Elements of Z-module reasoning
-
41
-
Learning and applying generalised solutions using higher order resolution
-
61
-
Specifying theorem provers in a higher-order logic programming language
-
81
-
Query processing in quantitative logic programming
-
101
-
An environment for automated reasoning about partial functions
-
111
-
The use of explicit plans to guide inductive proofs
-
121
-
Logicalc: An environment for interactive proof development
-
131
-
Implementing verification strategies in the KIV-system
-
141
-
Checking natural language proofs
-
151
-
Consistency of rule-based expert systems
-
162
-
A mechanizable induction principle for equational specifications
-
182
-
Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time
-
197
-
Towards efficient "knowledge-based" automated theorem proving for non-standard logics
-
218
-
Propositional temporal interval logic is PSPACE complete
-
238
-
Computational metatheory in Nuprl
-
258
-
Type inference in Prolog
-
278
-
Procedural interpretation of non-horn logic programs
-
294
-
Recursive query answering with non-horn clauses
-
313
-
Case inference in resolution-based languages
-
323
-
Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machine
-
333
-
Exploitation of parallelism in prototypical deduction problems
-
344
-
A decision procedure for unquantified formulas of graph theory
-
358
-
Adventures in associative-commutative unification (A summary)
-
368
-
Unification in finite algebras is unitary(?)
-
378
-
Unification in a combination of arbitrary disjoint equational theories
-
397
-
Partial unification for graph based equational reasoning
-
415
-
SATCHMO: A theorem prover implemented in Prolog
-
435
-
Term rewriting: Some experimental results
-
454
-
Analogical reasoning and proof discovery
-
469
-
Hyper-chaining and knowledge-based theorem proving
-
487
-
Linear modal deductions
-
500
-
A resolution calculus for modal logics
-
517
-
Solving disequations in equational theories
-
527
-
On word problems in Horn theories
-
538
-
Canonical conditional rewrite systems
-
550
-
Program synthesis by completion with dependent subtypes
-
563
-
Reasoning about systems of linear inequalities
-
573
-
A subsumption algorithm based on characteristic matrices
-
582
-
A restriction of factoring in binary resolution
-
592
-
Supposition-based logic for automated nonmonotonic reasoning
-
602
-
Argument-bounded algorithms as a basis for automated termination proofs
-
622
-
Two automated methods in implementation proofs
-
643
-
A new approach to universal unfication and its application to AC-unification
-
658
-
An implementation of a dissolution-based system employing theory links
-
675
-
Decision procedure for autoepistemic logic
-
685
-
Logical matrix generation and testing
-
694
-
Optimal time bounds for parallel term matching
-
704
-
Challenge equality problems in lattice theory
-
710
-
Single axioms in the implicational propositional calculus
-
714
-
Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs
-
730
-
Challenge problems from nonassociative rings for theorem provers
-
735
-
An interactive enhancement to the Boyer-Moore theorem prover
-
737
-
A goal directed theorem prover
-
738
-
m-NEVER system summary
-
740
-
EFS — An interactive Environment for Formal Systems
-
742
-
Ontic: A knowledge representation system for mathematics
-
744
-
Some tools for an inference laboratory (ATINF)
-
746
-
Quantlog: A system for approximate reasoning in inconsistent formal systems
-
748
-
LP: The larch prover
-
750
-
The KLAUS automated deduction system
-
752
-
A Prolog technology theorem prover
-
754
-
λProlog: An extended logic programming language
-
756
-
SYMEVAL: A theorem prover based on the experimental logic
-
758
-
ZPLAN: An automatic reasoning system for situations
-
760
-
The TPS theorem proving system
-
762
-
MOLOG: A modal PROLOG
-
764
-
PARTHENON: A parallel theorem prover for non-horn clauses
-
766
-
An nH-Prolog implementation
-
768
-
RRL: A rewrite rule laboratory
-
770
-
Geometer: A theorem prover for algebraic geometry
-
772
-
Isabelle: The next seven hundred theorem provers
-
774
-
The CHIP system : Constraint handling in Prolog
