Logic Programming and Automated Reasoning
Springer Berlin (Verlag)
978-3-540-55727-2 (ISBN)
Soundness and completeness of partial deductions for well-founded semantics.- On deductive planning and the frame problem.- On resolution in fragments of classical linear logic (extended abstract).- A procedure for automatic proof nets construction.- Free logic and infinite constraint networks.- Towards probabilistic knowledge bases.- Two-level grammar: A functional/logic query language for database and knowledge-base systems.- Extending deductive database languages by embedded implications.- Controlling redundancy in large search spaces: Argonne-style theorem proving through the years.- Resolution for many-valued logics.- An ordered theory resolution calculus.- Application of automated deduction to the search for single axioms for exponent groups.- Elementary lower bounds for the lengths of refutations.- Shortening proofs by quantifier introduction.- Reform compilation for nonlinear recursion.- Pruning infinite failure branches in programs with occur-check.- The use of planning critics in mechanizing inductive proofs.- ??-Calculus: An algorithmic interpretation of classical natural deduction.- Building proofs by analogy via the Curry-Howard Isomorphism.- On the use of the constructive omega-rule within automated deduction.- OR-parallel theorem proving with random competition.- Parallel computation of multiple sets-of-support.- Towards using the Andorra Kernel Language for industrial real-time applications.- Unification in a combination of equational theories with shared constants and its application to primal algebras.- Non-clausal resolution and superposition with selection and redundancy criteria.- Relating innermost, weak, uniform and modular termination of term rewriting systems.- A two steps semantics for logic programs with negation.- Generalized negation asfailure and semantics of normal disjunctive logic programs.- General model theoretic semantics for Higher-Order horn logic programming.- Disjunctive deductive databases.- Netlog - A concept oriented logic programming language.- From the past to the future: Executing temporal logic programs.- Computing induction axioms.- Consistency of equational enrichments.- A programming logic for a verified structured assembly language.- The unification of infinite sets of terms and its applications.- Unification in order-sorted type theory.- Infinite, canonical string rewriting systems generated by completion.- Spes: A system for logic program transformation.- Linear Objects: A logic framework for open system programming.- ISAR: An interactive system for algebraic implementation proofs.- Mathpert: Computer support for learning algebra, trig, and calculus.- MegaLog - A platform for developing knowledge base management systems.- SPIKE, an automatic theorem prover.- An application to teaching in logic course of ATP based on natural deduction.- A generic logic environment.- ElipSys A parallel programming system based on logic.- Opium - A high-level debugging environment.- An inductive theorem prover based on narrowing.- A cooperative answering system.- MIZ-PR: A theorem prover for polymorphic and recursive functions.- ProPre A programming language with proofs.- FRIENDLY-WAM: An interactive tool to understand the compilation of PROLOG.- SEPIA - a Basis for Prolog extensions.- The external database in SICStus Prolog.- The KCM system: Speeding-up logic programming through hardware support.- Logician's Workbench.- EUODHILOS: A general reasoning system for a variety of logics.- The EKS-V1 system.- CHIP and Propia.
| Erscheint lt. Verlag | 1.7.1992 |
|---|---|
| Reihe/Serie | Lecture Notes in Artificial Intelligence | Lecture Notes in Computer Science |
| Zusatzinfo | XVI, 516 p. |
| Verlagsort | Berlin |
| Sprache | englisch |
| Maße | 155 x 233 mm |
| Gewicht | 770 g |
| Themenwelt | Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik |
| Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre | |
| Schlagworte | Artificial Intelligence • Automat • automated reasoning • Automated Theorem Proving • Automatisches Beweisen • Automatisches Beweisverfahren • Automatisches Schliessen • Automatisches Schließen • Datenbank • Deductive Databases • Deduktive Datenbanken • Hardcover, Softcover / Informatik, EDV/Informatik • HC/Informatik, EDV/Informatik • Künstliche Intelligenz • Logic • Logic Programming • Logik • Logische Programmierung • Logisches Programmieren • Mathematische Logik • Nichtklassische Logik • Non-Classical Logics • Nonmonotonic Reasoning • Programmierung • programming • proving • Theorembeweisen (Kybern.) • theorem proving |
| ISBN-10 | 3-540-55727-X / 354055727X |
| ISBN-13 | 978-3-540-55727-2 / 9783540557272 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
