This book constitutes the refereed proceedings of the 13th International Conference on Automated Deduction, CADE-13, held in July/August 1996 in New Brunswick, NJ, USA, as part of FLoC '96.
The volume presents 46 revised regular papers selected from a total of 114 submissions in this category; also included are 15 selected system descriptions and abstracts of two invited talks. The CADE conferences are the major forum for the presentation of new results in all aspects of automated deduction. Therefore, the volume is a timely report on the state-of-the-art in the area.
Author(s): Harald Ganzinger (auth.), M. A. McRobbie, J. K. Slaney (eds.)
Series: Lecture Notes in Computer Science 1104 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1996
Language: English
Pages: 772
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Mathematical Logic and Foundations
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
