10th International Conference on Automated Deduction - neues Buch

EAN (ISBN-13): 9783540471714
Herausgeber: Springer Science+Business Media

Buch in der Datenbank seit 2017-06-04T22:30:31+02:00 (Berlin)
Detailseite zuletzt geändert am 2021-10-13T16:48:30+02:00 (Berlin)
ISBN/EAN: 9783540471714

ISBN - alternative Schreibweisen:
978-3-540-47171-4
Alternative Schreibweisen und verwandte Suchbegriffe:
Titel des Buches: international

---

Daten vom Verlag:

Autor/in: Mark E. Stickel
Titel: Lecture Notes in Computer Science; Lecture Notes in Artificial Intelligence; 10th International Conference on Automated Deduction - Kaiserslautern, FRG, July 24-27, 1990. Proceedings
Verlag: Springer; Springer Berlin
690 Seiten
Erscheinungsjahr: 2005-07-06
Berlin; Heidelberg; DE
Sprache: Englisch
139,09 € (DE)
143,00 € (AT)
165,50 CHF (CH)
Available
XVIII, 690 p.

EA; E107; eBook; Nonbooks, PBS / Informatik, EDV/Informatik; Künstliche Intelligenz; Verstehen; Artificial intelligence; Automat; Resolution; automated deduction; intelligence; logic; programming; proving; theorem proving; verification; C; Artificial Intelligence; Formal Languages and Automata Theory; Computer Science; Theoretische Informatik; BC

A theorem prover for a computational logic.- A complete semantic back chaining proof system.- Parallelizing the closure computation in automated deduction.- Partheo: A high-performance parallel theorem prover.- Substitution-based compilation of extended rules in deductive databases.- Automatic theorem proving in paraconsistent logics: Theory and implementation.- Case-free programs: An abstraction of definite horn programs.- Generalized well-founded semantics for logic programs.- Tactical theorem proving in program verification.- Extensions to the rippling-out tactic for guiding inductive proofs.- Guiding induction proofs.- Term rewriting induction.- A resolution principle for clauses with constraints.- Str+ve $$\\subseteq$$ : The Str+ve-based subset prover.- Ritt-Wu's decomposition algorithm and geometry theorem proving.- Encoding a dependent-type ?-calculus in a logic programming language.- Investigations into proof-search in a system of first-order dependent function types.- Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete.- An improved general E-unification method.- Some results on equational unification.- Unification in a combination of equational theories: an efficient algorithm.- SLIM: An automated reasoner for equivalences, applied to set theory.- An examination of the prolog technology theorem-prover.- Presenting intuitive deductions via symmetric simplification.- Toward mechanical methods for streamlining proofs.- Ordered rewriting and confluence.- Complete sets of reductions with constraints.- Rewrite systems for varieties of semigroups.- Improving associative path orderings.- Perspectives on automated deduction.- On restrictions of ordered paramodulation with simplification.-Simultaneous paramodulation.- Hyper resolution and equality axioms without function substitutions.- Automatic acquisition of search guiding heuristics.- Automated reasoning contributes to mathematics and logic.- A mechanically assisted constructive proof in category theory.- Dynamic logic as a uniform framework for theorem proving in intensional logic.- A tableaux-based theorem prover for a decidable subset of default logic.- Computing prime implicants.- Minimizing the number of clauses by renaming.- Higher order E-unification.- Programming by example and proving by example using higher-order unification.- Retrieving library identifiers via equational matching of types.- Unification in monoidal theories.- A science of reasoning: Extended abstract.- The TPS theorem proving system.- Schemata.- Cylindric algebra equation solver.- The OYSTER-CLAM system.- A high-performance parallel theorem prover.- The romulus proof checker.- IMPS : An interactive mathematical proof system.- UNICOM: A refined completion based inductive theorem prover.- The theorem prover of the program verifier Tatzelwurm.- RCL: A lisp verification system.- Orme an implementation of completion procedures as sets of transitions rules.- Otter 2.0.- Dissolver: A dissolution-based theorem prover.- TRIP: An implementation of clausal rewriting.- OSCAR.- Expert thinker: An adaptation of F-Prolog to microcomputers.- A prolog technology theorem prover.- A general clause theorem prover.- Liss — The logic inference search system.- ACE: The abstract clause engine.- Tutorial on high-performance automated theorem proving.- Tutorial on reasoning and representation with concept languages.- Tutorial on ?Prolog.- Tutorial on equational unification.- Tutorial on compilation techniques for logics.- Tutorial onhigh-performance theorem provers: Efficient implementation and parallelisation.- Tutorial on rewrite-based theorem proving.- Tutorial on program-synthetic deduction.- Tutorial on computing models of propositional logics.
Proceedings of CADE-10. CADE is the major forum for research on all aspects of automated deduction. The CADE conferences have no peer in the concentration and quality of their automated deduction research contributions.