Automated deduction - CADE-15 : 15th International Conference on Automated Deduction Lindau, Germany, July 5 10, 1998 : proceedings
This book constitutes the refereed proceedings of the 15th International Conference on Automated Deduction, CADE-15, held in Lindau, Germany, in July 1998. The volume presents three invited contributions together with 25 revised full papers and 10 revised system descriptions; these were selected fro...
Guardat en:
| Autor corporatiu: | |
|---|---|
| Altres autors: | , |
| Format: | Livre numérique |
| Idioma: | Anglais |
| Publicat: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Col·lecció: | Lecture notes in computer science. Lecture notes in artificial intelligence
1421 |
| Matèries: | |
| Accés en línia: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
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-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, proceedings, Claude Kirchner, Hélène Kirchner (Eds.), 1998, Berlin, Springer, 1 vol. (XIV-441 p.), Lecture notes in computer science, 3-540-64675-2 • Automated Deduction - CADE-15, Texte imprimé, 9783662196786 |
Taula de continguts:
- Reasoning about deductions in linear logic
- A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia
- Proving geometric theorems using clifford algebra and rewrite rules
- System description: similarity-based lemma generation for model elimination
- System description: Verification of distributed Erlang programs
- System description: Cooperation in model elimination: CPTHEO
- System description: CardTAP: The first theorem prover on a smart card
- System description: leanK 2.0
- Extensional higher-order resolution
- X.R.S: Explicit reduction systems A first-order calculus for higher-order calculi
- About the confluence of equational pattern rewrite systems
- Unification in lambda-calculi with if-then-else
- System description: An equational constraints solver
- System description: CRIL platform for SAT
- System description: Proof planning in higher-order logic with ?Clam
- System description: An interface between CLAM and HOL
- System description: Leo A higher-order theorem prover
- Superposition for divisible torsion-free abelian groups
- Strict basic superposition
- Elimination of equality via transformation with ordering constraints
- A resolution decision procedure for the guarded fragment
- Combining Hilbert style and semantic reasoning in a resolution framework
- ACL2 support for verification projects
- A fast algorithm for uniform semi-unification
- Termination analysis by inductive evaluation
- Admissibility of fixpoint induction over partial types
- Automated theorem proving in a simple meta-logic for LF
- Deductive vs. model-theoretic approaches to formal verification
- Automated deduction of finite-state control programs for reactive systems
- A proof environment for the development of groupcommunication systems
- On the relationship between non-horn magic sets and relevancy testing
- Certified version of Buchberger's algorithm
- Selectively instantiating definitions
- Using matings for pruning connection tableaux
- On generating small clause normal forms
- Rank/activity: A canonical form for binary resolution
- Towards efficient subsumption.