This volume contains the reviewed papers presented at the 12th International Conference on Automated Deduction (CADE-12) held at Nancy, France in June/July 1994.
The 67 papers presented were selected from 177 submissions and document many of the most important research results in automated deduction since CADE-11 was held in June 1992. The volume is organized in chapters on heuristics, resolution systems, induction, controlling resolutions, ATP problems, unification, LP applications, special-purpose provers, rewrite rule termination, ATP efficiency, AC unification, higher-order theorem proving, natural systems, problem sets, and system descriptions.
Author(s): John Slaney (auth.), Alan Bundy (eds.)
Series: Lecture Notes in Computer Science 814 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1994
Language: English
Pages: 852
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Mathematical Logic and Foundations
The crisis in finite mathematics: Automated reasoning as cause and cure....Pages 1-13
A divergence critic....Pages 14-28
Synthesis of induction orderings for existence proofs....Pages 29-41
Lazy generation of induction hypotheses....Pages 42-56
The search efficiency of theorem proving strategies....Pages 57-71
A method for building models automatically. Experiments with an extension of OTTER....Pages 72-86
Model elimination without contrapositives....Pages 87-101
Induction using term orderings....Pages 102-117
Mechanizable inductive proofs for a class of ∀ ∃ formulas....Pages 118-132
On the connection between narrowing and proof by consistency....Pages 133-147
A fixedpoint approach to implementing (Co)inductive definitions....Pages 148-161
On notions of inductive validity for first-order equational clauses....Pages 162-176
A new application for explanation-based generalisation within automated deduction....Pages 177-191
Semantically guided first-order theorem proving using hyper-linking....Pages 192-206
The applicability of logic program analysis and transformation to theorem proving....Pages 207-221
Detecting non-provable goals....Pages 222-236
A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?....Pages 237-251
The TPTP problem library....Pages 252-266
Combination techniques for non-disjoint equational theories....Pages 267-281
Primal grammars and unification modulo a binary clause....Pages 282-295
Conservative query normalization on parallel circumscription....Pages 296-310
Bottom-up evaluation of Datalog programs with arithmetic constraints....Pages 311-325
On intuitionistic query answering in description bases....Pages 326-340
Deductive composition of astronomical software from subroutine libraries....Pages 341-355
Proof script pragmatics in IMPS....Pages 356-370
A mechanization of strong Kleene logic for partial functions....Pages 371-385
Algebraic factoring and geometry theorem proving....Pages 386-400
Mechanically proving geometry theorems using a combination of Wu's method and Collins' method....Pages 401-415
Str∔ve and integers....Pages 416-430
What is a proof?....Pages 431-431
Termination, geometry and invariants....Pages 432-434
Ordered chaining for total orderings....Pages 435-450
Simple termination revisited....Pages 451-465
Termination orderings for rippling....Pages 466-483
A novel asynchronous parallelism scheme for first-order logic....Pages 484-498
Proving with BDDs and control of information....Pages 499-513
Extended path-indexing....Pages 514-528
Exporting and reflecting abstract metamathematics....Pages 529-529
Associative-commutative deduction with constraints....Pages 530-544
AC-superposition with constraints: No AC-unifiers needed....Pages 545-559
The complexity of counting problems in equational matching....Pages 560-574
Representing proof transformations for program optimization....Pages 575-589
Exploring abstract algebra in constructive type theory....Pages 590-604
Tactic theorem proving with refinement-tree proofs and metavariables....Pages 605-619
Unification in an extensional lambda calculus with ordered function sorts and constant overloading....Pages 620-634
Decidable higher-order unification problems....Pages 635-649
Theory and practice of minimal modular higher-order E -unification....Pages 650-664
A refined version of general E-unification....Pages 665-677
A completion-based method for mixed universal and rigid E -unification....Pages 678-692
On pot, pans and pudding or how to discover generalised critical Pairs....Pages 693-707
Semantic tableaux with ordering restrictions....Pages 708-722
Strongly analytic tableaux for normal modal logics....Pages 723-737
Reconstructing proofs at the assertion level....Pages 738-752
Problems on the generation of finite models....Pages 753-757
Combining symbolic computation and theorem proving: Some problems of Ramanujan....Pages 758-763
SCOTT: Semantically constrained otter system description....Pages 764-768
Protein: A PRO ver with a T heory E xtension IN terface....Pages 769-773
DELTA — A bottom-up preprocessor for top-down theorem provers....Pages 774-777
SETHEO V3.2: Recent developments....Pages 778-782
KoMeT....Pages 783-787
Ω-MKRP: A proof development environment....Pages 788-792
Lean T A P : Lean tableau-based theorem proving....Pages 793-797
FINDER: Finite domain enumerator system description....Pages 798-801
Symlog automated advice in Fitch-style proof construction....Pages 802-806
KEIM: A toolkit for automated deduction....Pages 807-810
Elf: A meta-language for deductive systems....Pages 811-815
EUODHILOS-II on top of GNU epoch....Pages 816-820
Pi: An interactive derivation editor for the calculus of partial inductive definitions....Pages 821-825
Mollusc a general proof-development shell for sequent-based logics....Pages 826-830
KITP-93: An automated inference system for program analysis....Pages 831-835
SPIKE: A system for sufficient completeness and parameterized inductive proofs....Pages 836-840
Distributed theorem proving by Peers ....Pages 841-845
