Automated Deduction — Cade-13: 13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30 – August 3, 1996 Proceedings

Saturation-based theorem proving: Past successes and future potential....Pages 1-1
A resolution theorem prover for intuitionistic logic....Pages 2-16
Proof-terms for classical and intuitionistic resolution....Pages 17-31
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E -unification....Pages 32-46
Extensions to a generalization critic for inductive proof....Pages 47-61
Learning domain knowledge to improve theorem proving....Pages 62-76
Patching faulty conjectures....Pages 77-91
Internal analogy in theorem proving....Pages 92-105
Termination of theorem proving by reuse....Pages 106-120
Termination of algorithms over non-freely generated data types....Pages 121-135
ABSFOL: A proof checker with abstraction....Pages 136-140
SPASS & FLOTTER version 0.42....Pages 141-145
The design of the CADE-13 ATP system competition....Pages 146-160
SCAN—Elimination of predicate quantifiers....Pages 161-165
GEOTHER: A geometry theorem prover....Pages 166-170
Structuring metatheory on inductive definitions....Pages 171-185
An embedding of Ruby in Isabelle....Pages 186-200
Mechanical verification of mutually recursive procedures....Pages 201-215
FasTraC a decentralized traffic control system based on logic programming....Pages 216-220
Presenting machine-found proofs....Pages 221-225
MUltlog 1.0: Towards an expert system for many-valued logics....Pages 226-230
CtCoq: A system presentation....Pages 231-234
An introduction to geometry expert....Pages 235-239
SiCoTHEO: Simple competitive parallel theorem provers....Pages 240-244
What can we hope to achieve from automated deduction?....Pages 245-245
Unification algorithms cannot be combined in polynomial time....Pages 246-260
Unification and matching modulo nilpotence....Pages 261-274
An improved lower bound for the elementary theories of trees....Pages 275-287
INKA: The next generation....Pages 288-292
XRay: A prolog technology theorem prover for default reasoning: A system description....Pages 293-297
IMPS: An updated system description....Pages 298-302
The tableau-based theorem prover 3 T A P Version 4.0....Pages 303-307
System description generating models by SEM....Pages 308-312
Optimizing proof search in model elimination....Pages 313-327
An abstract machine for fixed-order dynamically stratified programs....Pages 328-342
Unification in pseudo-linear sort theories is decidable....Pages 343-357
Theorem proving with group presentations: Examples and questions....Pages 358-372
Transforming termination by self-labelling....Pages 373-387
Theorem proving in cancellative abelian monoids (extended abstract)....Pages 388-402
On the practical value of different definitional translations to normal form....Pages 403-417
Converting non-classical matrix proofs into sequent-style systems....Pages 418-432
Efficient model generation through compilation....Pages 433-447
Algebra and automated deduction....Pages 448-462
On Shostak's decision procedure for combinations of theories....Pages 463-477
Ground resolution with group computations on semantic symmetries....Pages 478-492
A new method for knowledge compilation: The achievement by cycle search....Pages 493-507
Rewrite semantics for production rule systems: Theory and applications....Pages 508-522
Experiments in the heuristic use of past proof experience....Pages 523-537
Lemma discovery in automating induction....Pages 538-552
Advanced indexing operations on substitution trees....Pages 553-567
Semantic trees revisited: Some new completeness results....Pages 568-582
Building decision procedures for modal logics from propositional decision procedures — The case study of modal K....Pages 583-597
Resolution-based calculi for modal and temporal logics....Pages 598-612
Tableaux and algorithms for Propositional Dynamic Logic with Converse....Pages 613-627
Reflection of formal tactics in a deductive reflection framework....Pages 628-642
Walther recursion....Pages 643-657
Proof search with set variable instantiation in the Calculus of Constructions....Pages 658-672
Search strategies for resolution in temporal logics....Pages 673-687
Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices....Pages 688-702
Grammar specification in categorial logics and theorem proving....Pages 703-717
Path indexing for AC-theories....Pages 718-732
More Church-Rosser proofs (in Isabelle/HOL)....Pages 733-747
Partitioning methods for satisfiability testing on large formulas....Pages 748-762