Automated Deduction - CADE-15 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Kirchner, Claude (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Kirchner, Helene (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1998.
• Έκδοση: 1st ed. 1998.
• Σειρά: Lecture Notes in Artificial Intelligence ; 1421
• Θέματα: Artificial intelligence.; Mathematical logic.; Computer logic.; Artificial Intelligence.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.

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...

Πίνακας περιεχομένων:

• 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 group communication 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.