Willkommen, schön sind Sie da!
Logo Ex Libris

8th International Conference on Automated Deduction

  • Kartonierter Einband
  • 724 Seiten
(0) Erste Bewertung abgeben
Bewertungen & Rezensionen
(0)
(0)
(0)
(0)
(0)
Alle Bewertungen ansehen
InhaltConnections and higher-order logic.- Commutation, transformation, and termination.- Full-commutation and fair-termination in... Weiterlesen
20%
115.00 CHF 92.00
Sie sparen CHF 23.00
Print on Demand - Auslieferung erfolgt in der Regel innert 4 bis 6 Wochen.
Bestellung & Lieferung in eine Filiale möglich

Beschreibung

Inhalt
Connections and higher-order logic.- Commutation, transformation, and termination.- Full-commutation and fair-termination in equational (and combined) term-rewriting systems.- An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations.- Proving termination of associative commutative rewriting systems by rewriting.- Relating resolution and algebraic completion for Horn logic.- A simple non-termination test for the Knuth-Bendix method.- A new formula for the execution of categorical combinators.- Proof by induction using test sets.- How to prove equivalence of term rewriting systems without induction.- Sufficient completeness, term rewriting systems and anti-unification.- A new method for establishing refutational completeness in theorem proving.- A theory of diagnosis from first principles.- Some contributions to the logical analysis of circumscription.- Modal theorem proving.- Computational aspects of three-valued logic.- Resolution and quantified epistemic logics.- A commonsense theory of nonmonotonic reasoning.- Negative paramodulation.- The heuristics and experimental results of a new hyperparamodulation: HL-resolution.- ECR: An equality conditional resolution proof procedure.- Using narrowing to do isolation in symbolic equation solving an experiment in automated reasoning.- Formulation of induction formulas in verification of prolog programs.- Program verifier "Tatzelwurm": Reasoning about systems systems of linear inequalities.- An interactive verification system based on dynamic logic.- What you always wanted to know about clause graph resolution.- Parallel theorem proving with connection graphs.- Theory links in semantic graphs.- Abstraction using generalization functions.- An improvement of deduction plans: Refutation plans.- Controlling deduction with proof condensation and heuristics.- Nested resolution.- Mechanizing constructive proofs.- Implementing number theory: An experiment with Nuprl.- Parallel algorithms for term matching.- Unification in combinations of collapse-free theories with disjoint sets of function symbols.- Combination of unification algorithms.- Unification in the data structure sets.- NP-completeness of the set unification and matching problems.- Matching with distributivity.- Unification in boolean rings.- Some relationships between unification, restricted unification, and matching.- A classification of many-sorted unification problems.- Unification in many-sorted equational theories.- Classes of first order formulas under various satisfiability definitions.- Diamond formulas in the dynamic logic of recursively enumerable programs.- A prolog machine.- A prolog technology theorem prover: Implementation by an extended prolog compiler.- Paths to high-performance automated theorem proving.- Purely functional implementation of a logic.- Causes for events: Their computation and applications.- How to clear a block: Plan formation in situational logic.- Deductive synthesis of sorting programs.- The TPS theorem proving system.- Trspec: A term rewriting based system for algebraic specifications.- Highly parallel inference machine.- Automatic theorem proving in the ISDV system.- The karlsruhe induction theorem proving system.- Overview of a theorem-prover for a computational logic.- GEO-prover A geometry theorem prover developed at UT.- The markgraf karl refutation procedure (MKRP).- The J-machine: Functional programming with combinators.- The illinois prover: A general purpose resolution theorem prover.- Theorem proving systems of the Formel project.- The passau RAP system: Prototyping algebraic specifications using conditional narrowing.- RRL: A rewrite rule laboratory.- A geometry theorem prover based on Buchberger's algorithm.- REVE a rewrite rule laboratory.- ITP at argonne national laboratory.- Autologic at university of victoria.- Thinker.- The KLAUS automated deduction system.- The KRIPKE automated theorem proving system.- SHD-prover at university of texas at austin.

Produktinformationen

Titel: 8th International Conference on Automated Deduction
Untertitel: Oxford, England, July 27- August 1, 1986. Proceedings
Editor:
EAN: 9783540167808
ISBN: 3540167803
Format: Kartonierter Einband
Herausgeber: Springer Berlin Heidelberg
Genre: Informatik
Anzahl Seiten: 724
Gewicht: 1077g
Größe: H235mm x B155mm x T38mm
Jahr: 1986
Untertitel: Englisch
Auflage: 1986

Weitere Produkte aus der Reihe "Lecture Notes in Computer Science"