10th International Conference on Automated Deduction: Kaiserslautern, FRG, July 24-27, 1990. Proceedings (Lecture Notes in Computer Science, 449, Band 449) - edizione con copertina flessibile

EAN (ISBN-13): 9783540528852
ISBN (ISBN-10): 3540528857
Copertina flessibile
Anno di pubblicazione: 1990
Editore: Springer Berlin Heidelberg
688 Pagine
Peso: 1,052 kg

Libro nella banca dati dal 2007-06-21T06:03:27+02:00 (Rome)
Pagina di dettaglio ultima modifica in 2023-11-20T20:52:51+01:00 (Rome)
ISBN/EAN: 3540528857

ISBN - Stili di scrittura alternativi:
3-540-52885-7, 978-3-540-52885-2
Stili di scrittura alternativi e concetti di ricerca simili:
Autore del libro : stickel
Titolo del libro: 10th, deduction, july july, tenth, international conference computer science, kaiserslautern, frg, proceedings artificial intelligence conference, lecture notes artificial intelligence

---

Dati dell'editore

Autore: Mark E. Stickel
Titolo: Lecture Notes in Computer Science; Lecture Notes in Artificial Intelligence; 10th International Conference on Automated Deduction - Kaiserslautern, FRG, July 24-27, 1990. Proceedings
Editore: Springer; Springer Berlin
690 Pagine
Anno di pubblicazione: 1990-07-17
Berlin; Heidelberg; DE
Lingua: Inglese
149,79 € (DE)
153,99 € (AT)
165,50 CHF (CH)
Available
XVIII, 690 p.

BC; Hardcover, Softcover / Informatik, EDV/Informatik; Künstliche Intelligenz; Verstehen; Artificial intelligence; Automat; Resolution; automated deduction; intelligence; logic; programming; proving; theorem proving; verification; Artificial Intelligence; Formal Languages and Automata Theory; Theoretische Informatik; EA

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.