9th International Conference on Automated Deduction
Springer Berlin (Verlag)
978-3-540-19343-2 (ISBN)
First-order theorem proving using conditional rewrite rules.- Elements of Z-module reasoning.- Learning and applying generalised solutions using higher order resolution.- Specifying theorem provers in a higher-order logic programming language.- Query processing in quantitative logic programming.- An environment for automated reasoning about partial functions.- The use of explicit plans to guide inductive proofs.- Logicalc: An environment for interactive proof development.- Implementing verification strategies in the KIV-system.- Checking natural language proofs.- Consistency of rule-based expert systems.- A mechanizable induction principle for equational specifications.- Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time.- Towards efficient "knowledge-based" automated theorem proving for non-standard logics.- Propositional temporal interval logic is PSPACE complete.- Computational metatheory in Nuprl.- Type inference in Prolog.- Procedural interpretation of non-horn logic programs.- Recursive query answering with non-horn clauses.- Case inference in resolution-based languages.- Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machine.- Exploitation of parallelism in prototypical deduction problems.- A decision procedure for unquantified formulas of graph theory.- Adventures in associative-commutative unification (A summary).- Unification in finite algebras is unitary(?).- Unification in a combination of arbitrary disjoint equational theories.- Partial unification for graph based equational reasoning.- SATCHMO: A theorem prover implemented in Prolog.- Term rewriting: Some experimental results.- Analogical reasoning and proof discovery.- Hyper-chaining and knowledge-based theorem proving.- Linear modal deductions.- A resolution calculus for modal logics.- Solving disequations in equational theories.- On word problems in Horn theories.- Canonical conditional rewrite systems.- Program synthesis by completion with dependent subtypes.- Reasoning about systems of linear inequalities.- A subsumption algorithm based on characteristic matrices.- A restriction of factoring in binary resolution.- Supposition-based logic for automated nonmonotonic reasoning.- Argument-bounded algorithms as a basis for automated termination proofs.- Two automated methods in implementation proofs.- A new approach to universal unfication and its application to AC-unification.- An implementation of a dissolution-based system employing theory links.- Decision procedure for autoepistemic logic.- Logical matrix generation and testing.- Optimal time bounds for parallel term matching.- Challenge equality problems in lattice theory.- Single axioms in the implicational propositional calculus.- Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs.- Challenge problems from nonassociative rings for theorem provers.- An interactive enhancement to the Boyer-Moore theorem prover.- A goal directed theorem prover.- m-NEVER system summary.- EFS - An interactive Environment for Formal Systems.- Ontic: A knowledge representation system for mathematics.- Some tools for an inference laboratory (ATINF).- Quantlog: A system for approximate reasoning in inconsistent formal systems.- LP: The larch prover.- The KLAUS automated deduction system.- A Prolog technology theorem prover.- ?Prolog: An extended logic programming language.- SYMEVAL: A theorem prover based on the experimental logic.- ZPLAN: An automatic reasoning system forsituations.- The TPS theorem proving system.- MOLOG: A modal PROLOG.- PARTHENON: A parallel theorem prover for non-horn clauses.- An nH-Prolog implementation.- RRL: A rewrite rule laboratory.- Geometer: A theorem prover for algebraic geometry.- Isabelle: The next seven hundred theorem provers.- The CHIP system : Constraint handling in Prolog.
| Erscheint lt. Verlag | 4.5.1988 |
|---|---|
| Reihe/Serie | Lecture Notes in Computer Science |
| Zusatzinfo | X, 776 p. |
| Verlagsort | Berlin |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Gewicht | 1089 g |
| Themenwelt | Mathematik / Informatik ► Informatik ► Theorie / Studium |
| Mathematik / Informatik ► Mathematik ► Allgemeines / Lexika | |
| Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre | |
| Schlagworte | algorithms • automated deduction • Automated Theorem Proving • Deduktionssystem • Erfüllbarkeitsproblem der Aussagenlogik • Isabelle • Logic • Proof • Resolution • theorem proving |
| ISBN-10 | 3-540-19343-X / 354019343X |
| ISBN-13 | 978-3-540-19343-2 / 9783540193432 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
