Automated deduction : Cade-13 : 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996 : proceedings
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;...
Enregistré dans:
| Auteur principal: | |
|---|---|
| Collectivité auteur: | |
| Autres auteurs: | |
| Format: | Livre numérique |
| Langue: | Anglais |
| Publié: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Collection: | Lecture notes in computer science. Lecture notes in artificial intelligence
1104 |
| Sujets: | |
| Accès en ligne: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Note: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Automated deduction, CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996, proceedings, M.A. McRobbie, J.K. Slaney, eds, 1996, Berlin, Springer, 1 vol. (XV-764 p.), Lecture notes in computer science, 3-540-61511-3 • Automated Deduction - Cade-13, Texte imprimé, 9783662176726 |
Table des matières:
- Saturation-based theorem proving: Past successes and future potential
- A resolution theorem prover for intuitionistic logic
- Proof-terms for classical and intuitionistic resolution
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
- Extensions to a generalization critic for inductive proof
- Learning domain knowledge to improve theorem proving
- Patching faulty conjectures
- Internal analogy in theorem proving
- Termination of theorem proving by reuse
- Termination of algorithms over non-freely generated data types
- ABSFOL: A proof checker with abstraction
- SPASS & FLOTTER version 0.42
- The design of the CADE-13 ATP system competition
- SCAN Elimination of predicate quantifiers
- GEOTHER: A geometry theorem prover
- Structuring metatheory on inductive definitions
- An embedding of Ruby in Isabelle
- Mechanical verification of mutually recursive procedures
- FasTraC a decentralized traffic control system based on logic programming
- Presenting machine-found proofs
- MUltlog 1.0: Towards an expert system for many-valued logics
- CtCoq: A system presentation
- An introduction to geometry expert
- SiCoTHEO: Simple competitive parallel theorem provers
- What can we hope to achieve from automated deduction?
- Unification algorithms cannot be combined in polynomial time
- Unification and matching modulo nilpotence
- An improved lower bound for the elementary theories of trees
- INKA: The next generation
- XRay: A prolog technology theorem prover for default reasoning: A system description
- IMPS: An updated system description
- The tableau-based theorem prover 3 T A P Version 4.0
- System description generating models by SEM
- Optimizing proof search in model elimination
- An abstract machine for fixed-order dynamicallystratified programs
- Unification in pseudo-linear sort theories is decidable
- Theorem proving with group presentations: Examples and questions
- Transforming termination by self-labelling
- Theorem proving in cancellative abelian monoids (extended abstract)
- On the practical value of different definitional translations to normal form
- Converting non-classical matrix proofs into sequent-style systems
- Efficient model generation through compilation
- Algebra and automated deduction
- On Shostak's decision procedure for combinations of theories
- Ground resolution with group computations on semantic symmetries
- A new method for knowledge compilation: The achievement by cycle search
- Rewrite semantics for production rule systems: Theory and applications
- Experiments in the heuristic use of past proof experience
- Lemma discovery in automating induction
- Advanced indexing operations on substitution trees
- Semantic trees revisited: Some new completeness results
- Building decision procedures for modal logics from propositional decision procedures The case study of modal K
- Resolution-based calculi for modal and temporal logics
- Tableaux and algorithms for Propositional Dynamic Logic with Converse
- Reflection of formal tactics in a deductive reflection framework
- Walther recursion
- Proof search with set variable instantiation in the Calculus of Constructions
- Search strategies for resolution in temporal logics
- Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices
- Grammar specification in categorial logics and theorem proving
- Path indexing for AC-theories
- More Church-Rosser proofs (in Isabelle/HOL)
- Partitioning methods for satisfiability testing on large formulas.