Automated deduction : CADE-14 : 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 17, 1997 : proceedings
This book constitutes the strictly refereed proceedings of the 14th International Conference on Automated Deduction, CADE-14, held in Townsville, North Queensland, Australia, in July 1997. The volume presents 25 revised full papers selected from a total of 87 submissions; also included are 17 system...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Korporativní autor: | |
| Médium: | Livre numérique |
| Jazyk: | Anglais |
| Vydáno: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Edice: | Lecture notes in computer science. Lecture notes in artificial intelligence
1249 |
| Témata: | |
| On-line přístup: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Poznámka: |
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-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, proceedings, William McCune (Ed.), 1997, Berlin, Springer, 1 vol. (XIV-462 p.), Lecture notes in computer science, 3-540-63104-6 • Automated Deduction - CADE-14, Texte imprimé, 9783662179680 |
Obsah:
- The char-set method and its applications to automated reasoning
- Decidable call by need computations in term rewriting (extended abstract)
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- On equality up-to constraints over finite trees, context unification, and one-step rewriting
- Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses
- The Clause-Diffusion theorem prover Peers-mcd (system description)
- Integration of automated and interactive theorem proving in ILF
- ILF-SETHEO
- SETHEO goes software engineering: Application of ATP to software reuse
- Proving System Correctness with KIV 3.0
- A practical symbolic algorithm for the inverse kinematics of 6R manipulators with simple geometry
- Automatic verification of cryptographic protocols with SETHEO
- A practical integration of first-order reasoning and decision procedures
- Some pitfalls of LK-to-LJ translations and how to avoid them
- Deciding intuitionistic propositional logic via translation into classical logic
- Lemma matching for a PTTP-based top-down theorem prover
- Exact knowledge compilation in predicate calculus: The partial achievement case
- Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving
- Alternating automata: Unifying truth and validity checking for temporal logics
- Connection-based proof construction in linear logic
- Resource-distribution via Boolean constraints
- Constructing a normal form for Property Theory
- ?mega: Towards a mathematical assistant
- Plagiator A learning prover
- CODE: A powerful prover for problems of condensed detachment
- A new method for testing decision procedures in modal logics
- Minlog: A minimal logictheorem prover
- SATO: An efficient prepositional prover
- Using a generalisation critic to find bisimulations for coinductive proofs
- A colored version of the ?-calculus
- A practical implementation of simple consequence relations using inductive definitions
- Soft typing for ordered resolution
- A classification of non-liftable orders for resolution
- Hybrid interactive theorem proving using nuprl and HOL
- Proof tactics for a theory of state machines in a graphical environment
- RALL: Machine-supported proofs for relation algebra
- Nuprl-Light: An implementation framework for higher-order logics
- XIsabelle: A system description
- XBarnacle: Making theorem provers more accessible
- The tableau browser SNARKS
- Jape: A calculator for animating proof-on-paper
- Evolving combinators
- Partial matching for analogy discovery in proofs and counter-examples
- Dialog.