• Produktbild: Automated Deduction - CADE-14
  • Produktbild: Automated Deduction - CADE-14
Band 1249

Automated Deduction - CADE-14 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 - 17, 1997, Proceedings

49,99 €

inkl. gesetzl. MwSt., Versandkostenfrei


Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

18.06.1997

Abbildungen

XV, 469 p.

Herausgeber

William McCune

Verlag

Springer Berlin

Seitenzahl

469

Maße (L/B/H)

23,5/15,5/2,7 cm

Gewicht

727 g

Auflage

1997

Sprache

Englisch

ISBN

978-3-540-63104-0

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

18.06.1997

Abbildungen

XV, 469 p.

Herausgeber

William McCune

Verlag

Springer Berlin

Seitenzahl

469

Maße (L/B/H)

23,5/15,5/2,7 cm

Gewicht

727 g

Auflage

1997

Sprache

Englisch

ISBN

978-3-540-63104-0

Herstelleradresse

Springer-Verlag KG
Sachsenplatz 4-6
1201 Wien
AT

Email: ProductSafety@springernature.com

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)

  • Produktbild: Automated Deduction - CADE-14
  • Produktbild: Automated Deduction - CADE-14
  • The char-set method and its applications to automated reasoning.- Decidable call by need computations in term rewriting (extended abstract).- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method.- On equality up-to constraints over finite trees, context unification, and one-step rewriting.- Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses.- The Clause-Diffusion theorem prover Peers-mcd (system description).- Integration of automated and interactive theorem proving in ILF.- ILF-SETHEO.- SETHEO goes software engineering: Application of ATP to software reuse.- Proving System Correctness with KIV 3.0.- A practical symbolic algorithm for the inverse kinematics of 6R manipulators with simple geometry.- Automatic verification of cryptographic protocols with SETHEO.- A practical integration of first-order reasoning and decision procedures.- Some pitfalls of LK-to-LJ translations and how to avoid them.- Deciding intuitionistic propositional logic via translation into classical logic.- Lemma matching for a PTTP-based top-down theorem prover.- Exact knowledge compilation in predicate calculus: The partial achievement case.- Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving.- Alternating automata: Unifying truth and validity checking for temporal logics.- Connection-based proof construction in linear logic.- Resource-distribution via Boolean constraints.- Constructing a normal form for Property Theory.- ?mega: Towards a mathematical assistant.- Plagiator — A learning prover.- CODE: A powerful prover for problems of condensed detachment.- A new method for testing decision procedures in modal logics.- Minlog: A minimal logictheorem prover.- SATO: An efficient prepositional prover.- Using a generalisation critic to find bisimulations for coinductive proofs.- A colored version of the ?-calculus.- A practical implementation of simple consequence relations using inductive definitions.- Soft typing for ordered resolution.- A classification of non-liftable orders for resolution.- Hybrid interactive theorem proving using nuprl and HOL.- Proof tactics for a theory of state machines in a graphical environment.- RALL: Machine-supported proofs for relation algebra.- Nuprl-Light: An implementation framework for higher-order logics.- XIsabelle: A system description.- XBarnacle: Making theorem provers more accessible.- The tableau browser SNARKS.- Jape: A calculator for animating proof-on-paper.- Evolving combinators.- Partial matching for analogy discovery in proofs and counter-examples.- Dialog.