Automated deduction : CADE-12 : 12th International Conference on Automated Deduction, Nancy, France, June 26-July 1, 1994 : proceedings
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...
Enregistré dans:
| Auteur principal: | |
|---|---|
| Collectivité auteur: | |
| 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
814 |
| 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-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, proceedings, Alan Bundy (Ed.), Berlin, Springer-Verlag, 1994, 1 vol. (XVI-848 p.), Lecture notes in computer science, 3-540-58156-1 • Automated Deduction CADE-12, Texte imprimé, 9783662170083 |
Table des matières:
- The crisis in finite mathematics: Automated reasoning as cause and cure
- A divergence critic
- Synthesis of induction orderings for existence proofs
- Lazy generation of induction hypotheses
- The search efficiency of theorem proving strategies
- A method for building models automatically. Experiments with an extension of OTTER
- Model elimination without contrapositives
- Induction using term orderings
- Mechanizable inductive proofs for a class of ? ? formulas
- On the connection between narrowing and proof by consistency
- A fixedpoint approach to implementing (Co)inductive definitions
- On notions of inductive validity for first-order equational clauses
- A new application for explanation-based generalisation within automated deduction
- Semantically guided first-order theorem proving using hyper-linking
- The applicability of logic program analysis and transformation to theorem proving
- Detecting non-provable goals
- A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?
- The TPTP problem library
- Combination techniques for non-disjoint equational theories
- Primal grammars and unification modulo a binary clause
- Conservative query normalization on parallel circumscription
- Bottom-up evaluation of Datalog programs with arithmetic constraints
- On intuitionistic query answering in description bases
- Deductive composition of astronomical software from subroutine libraries
- Proof script pragmatics in IMPS
- A mechanization of strong Kleene logic for partial functions
- Algebraic factoring and geometry theorem proving
- Mechanically proving geometry theorems using a combination of Wu's method and Collins' method
- Str?ve and integers
- What is a proof?
- Termination, geometry and invariants
- Ordered chaining for totalorderings
- Simple termination revisited
- Termination orderings for rippling
- A novel asynchronous parallelism scheme for first-order logic
- Proving with BDDs and control of information
- Extended path-indexing
- Exporting and reflecting abstract metamathematics
- Associative-commutative deduction with constraints
- AC-superposition with constraints: No AC-unifiers needed
- The complexity of counting problems in equational matching
- Representing proof transformations for program optimization
- Exploring abstract algebra in constructive type theory
- Tactic theorem proving with refinement-tree proofs and metavariables
- Unification in an extensional lambda calculus with ordered function sorts and constant overloading
- Decidable higher-order unification problems
- Theory and practice of minimal modular higher-order E-unification
- A refined version of general E-unification
- A completion-based method for mixed universal and rigid E-unification
- On pot, pans and pudding or how to discover generalised critical Pairs
- Semantic tableaux with ordering restrictions
- Strongly analytic tableaux for normal modal logics
- Reconstructing proofs at the assertion level
- Problems on the generation of finite models
- Combining symbolic computation and theorem proving: Some problems of Ramanujan
- SCOTT: Semantically constrained otter system description
- Protein: A PROver with a Theory Extension INterface
- DELTA A bottom-up preprocessor for top-down theorem provers
- SETHEO V3.2: Recent developments
- KoMeT
- ?-MKRP: A proof development environment
- LeanT A P: Lean tableau-based theorem proving
- FINDER: Finite domain enumerator system description
- Symlog automated advice in Fitch-style proof construction
- KEIM: A toolkit for automated deduction
- Elf: Ameta-language for deductive systems
- EUODHILOS-II on top of GNU epoch
- Pi: An interactive derivation editor for the calculus of partial inductive definitions
- Mollusc a general proof-development shell for sequent-based logics
- KITP-93: An automated inference system for program analysis
- SPIKE: A system for sufficient completeness and parameterized inductive proofs
- Distributed theorem proving by Peers.