Automated Deduction ¿ CADE-12 | 12th International Conference on Automated Deduction Nancy, France, June 26¿July 1, 1994 Proceedings | Alan Bundy | Taschenbuch | Paperback | Englisch | 1994 - Taschenbuch

EAN (ISBN-13): 9783540581567
ISBN (ISBN-10): 3540581561
Taschenbuch
Erscheinungsjahr: 1994
Herausgeber: Springer Berlin

Buch in der Datenbank seit 2007-05-30T13:11:13+02:00 (Vienna)
Detailseite zuletzt geändert am 2023-10-03T17:30:52+02:00 (Vienna)
ISBN/EAN: 9783540581567

ISBN - alternative Schreibweisen:
3-540-58156-1, 978-3-540-58156-7
Alternative Schreibweisen und verwandte Suchbegriffe:
Titel des Buches: deduction, proceedings artificial intelligence conference, ded, lecture notes artificial intelligence, 814, cade

---

Daten vom Verlag:

Autor/in: Alan Bundy
Titel: Lecture Notes in Computer Science; Lecture Notes in Artificial Intelligence; Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings
Verlag: Springer; Springer Berlin
852 Seiten
Erscheinungsjahr: 1994-06-08
Berlin; Heidelberg; DE
Sprache: Englisch
53,49 € (DE)
54,99 € (AT)
59,00 CHF (CH)
Available
XVI, 852 p.

BC; Hardcover, Softcover / Informatik, EDV/Informatik; Künstliche Intelligenz; Verstehen; Automatisches Schließen; KI-Logiken; Logic Programming; Logisches Prorammieren; Term Rewriting; Term-Ersetzung; Theorem Proving; Variable; automated deduction; automated reasoning; complexity; grammar; heuristics; lambda calculus; proving; Artificial Intelligence; Formal Languages and Automata Theory; Mathematical Logic and Foundations; Theoretische Informatik; Mathematik: Logik; Mathematische Grundlagen; EA

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.