Del i serien Lecture Notes in Computer Science

Automated Deduction — CADE-12

12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings

Häftad, Engelska, 1994

739 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt för medlemmar vid köp för minst 249 kr.

This volume contains the reviewed papers presented at the 12th International Conference on Automated Deduction (CADE-12) held at Nancy, France in June/July 1994.The 67 papers presented were selected from 177 submissions and document many of the most important research results in automated deduction since CADE-11 was held in June 1992. The volume is organized in chapters on heuristics, resolution systems, induction, controlling resolutions, ATP problems, unification, LP applications, special-purpose provers, rewrite rule termination, ATP efficiency, AC unification, higher-order theorem proving, natural systems, problem sets, and system descriptions.

Produktinformation

Utgivningsdatum1994-06-08
Mått155 x 235 x 47 mm
Vikt1 293 g
FormatHäftad
SpråkEngelska
SerieLecture Notes in Computer Science
Antal sidor852
FörlagSpringer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN9783540581567

Tillhör följande kategorier

Artificiell intelligens inom Data och IT

The crisis in finite mathematics: Automated reasoning as cause and cure.- A divergence critic.- Synthesis of induction orderings for existence proofs.- Lazy generation of induction hypotheses.- The search efficiency of theorem proving strategies.- A method for building models automatically. Experiments with an extension of OTTER.- Model elimination without contrapositives.- Induction using term orderings.- Mechanizable inductive proofs for a class of ? ? formulas.- On the connection between narrowing and proof by consistency.- A fixedpoint approach to implementing (Co)inductive definitions.- On notions of inductive validity for first-order equational clauses.- A new application for explanation-based generalisation within automated deduction.- Semantically guided first-order theorem proving using hyper-linking.- The applicability of logic program analysis and transformation to theorem proving.- Detecting non-provable goals.- A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?.- The TPTP problem library.- Combination techniques for non-disjoint equational theories.- Primal grammars and unification modulo a binary clause.- Conservative query normalization on parallel circumscription.- Bottom-up evaluation of Datalog programs with arithmetic constraints.- On intuitionistic query answering in description bases.- Deductive composition of astronomical software from subroutine libraries.- Proof script pragmatics in IMPS.- A mechanization of strong Kleene logic for partial functions.- Algebraic factoring and geometry theorem proving.- Mechanically proving geometry theorems using a combination of Wu's method and Collins' method.- Str?ve and integers.- What is a proof?.- Termination, geometry and invariants.- Ordered chaining for totalorderings.- Simple termination revisited.- Termination orderings for rippling.- A novel asynchronous parallelism scheme for first-order logic.- Proving with BDDs and control of information.- Extended path-indexing.- Exporting and reflecting abstract metamathematics.- Associative-commutative deduction with constraints.- AC-superposition with constraints: No AC-unifiers needed.- The complexity of counting problems in equational matching.- Representing proof transformations for program optimization.- Exploring abstract algebra in constructive type theory.- Tactic theorem proving with refinement-tree proofs and metavariables.- Unification in an extensional lambda calculus with ordered function sorts and constant overloading.- Decidable higher-order unification problems.- Theory and practice of minimal modular higher-order E-unification.- A refined version of general E-unification.- A completion-based method for mixed universal and rigid E-unification.- On pot, pans and pudding or how to discover generalised critical Pairs.- Semantic tableaux with ordering restrictions.- Strongly analytic tableaux for normal modal logics.- Reconstructing proofs at the assertion level.- Problems on the generation of finite models.- Combining symbolic computation and theorem proving: Some problems of Ramanujan.- SCOTT: Semantically constrained otter system description.- Protein: A PROver with a Theory Extension INterface.- DELTA — A bottom-up preprocessor for top-down theorem provers.- SETHEO V3.2: Recent developments.- KoMeT.- ?-MKRP: A proof development environment.- LeanT A P: Lean tableau-based theorem proving.- FINDER: Finite domain enumerator system description.- Symlog automated advice in Fitch-style proof construction.- KEIM: A toolkit for automated deduction.- Elf: Ameta-language for deductive systems.- EUODHILOS-II on top of GNU epoch.- Pi: An interactive derivation editor for the calculus of partial inductive definitions.- Mollusc a general proof-development shell for sequent-based logics.- KITP-93: An automated inference system for program analysis.- SPIKE: A system for sufficient completeness and parameterized inductive proofs.- Distributed theorem proving by Peers.

Du kanske också är intresserad av

Sofia Petrovna

Lydia Chukovskaya

Häftad, 1994

609 kr

Foundation Pit

Andreai Platonovich Platonov, Mirra Ginsburg

Häftad, 1994

259 kr

Organic Dusts Exposure, Effects, and Prevention

Ragnar Rylander, Robert R. Jacobs

Inbunden, 1994

4 039 kr

Moral Dilemmas of Feminism

Laurie Shrage

Häftad, 1994

939 kr

Del 56

Rippling: Meta-Level Guidance for Mathematical Reasoning

Alan Bundy, David Basin, Dieter Hutter, Andrew Ireland

Inbunden, 2005

2 419 kr

Beyond Postmodern Politics

Honi Fern Haber

Häftad, 1994

939 kr

English-Deutsch

Hans-Joerg Salízites

Inbunden, 1994

1 739 kr

Artificial Intelligence Techniques

Alan Bundy

Häftad, 1996

739 kr

Ministry of Nurture

Duffy Robbins

Häftad, 1994

299 kr

Logical Foundations of Computer Science

Anil Nerode, Yu.V. Matiyasevich

Häftad, 1994

719 kr

Del i serien Lecture Notes in Computer Science

Automated Deduction — CADE-12

12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings

Häftad, Engelska, 1994

AvAlan Bundy

739 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt för medlemmar vid köp för minst 249 kr.

Produktinformation

Utgivningsdatum1994-06-08
Mått155 x 235 x 47 mm
Vikt1 293 g
FormatHäftad
SpråkEngelska
SerieLecture Notes in Computer Science
Antal sidor852
FörlagSpringer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN9783540581567

Tillhör följande kategorier

Artificiell intelligens inom Data och IT

The crisis in finite mathematics: Automated reasoning as cause and cure.- A divergence critic.- Synthesis of induction orderings for existence proofs.- Lazy generation of induction hypotheses.- The search efficiency of theorem proving strategies.- A method for building models automatically. Experiments with an extension of OTTER.- Model elimination without contrapositives.- Induction using term orderings.- Mechanizable inductive proofs for a class of ? ? formulas.- On the connection between narrowing and proof by consistency.- A fixedpoint approach to implementing (Co)inductive definitions.- On notions of inductive validity for first-order equational clauses.- A new application for explanation-based generalisation within automated deduction.- Semantically guided first-order theorem proving using hyper-linking.- The applicability of logic program analysis and transformation to theorem proving.- Detecting non-provable goals.- A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?.- The TPTP problem library.- Combination techniques for non-disjoint equational theories.- Primal grammars and unification modulo a binary clause.- Conservative query normalization on parallel circumscription.- Bottom-up evaluation of Datalog programs with arithmetic constraints.- On intuitionistic query answering in description bases.- Deductive composition of astronomical software from subroutine libraries.- Proof script pragmatics in IMPS.- A mechanization of strong Kleene logic for partial functions.- Algebraic factoring and geometry theorem proving.- Mechanically proving geometry theorems using a combination of Wu's method and Collins' method.- Str?ve and integers.- What is a proof?.- Termination, geometry and invariants.- Ordered chaining for totalorderings.- Simple termination revisited.- Termination orderings for rippling.- A novel asynchronous parallelism scheme for first-order logic.- Proving with BDDs and control of information.- Extended path-indexing.- Exporting and reflecting abstract metamathematics.- Associative-commutative deduction with constraints.- AC-superposition with constraints: No AC-unifiers needed.- The complexity of counting problems in equational matching.- Representing proof transformations for program optimization.- Exploring abstract algebra in constructive type theory.- Tactic theorem proving with refinement-tree proofs and metavariables.- Unification in an extensional lambda calculus with ordered function sorts and constant overloading.- Decidable higher-order unification problems.- Theory and practice of minimal modular higher-order E-unification.- A refined version of general E-unification.- A completion-based method for mixed universal and rigid E-unification.- On pot, pans and pudding or how to discover generalised critical Pairs.- Semantic tableaux with ordering restrictions.- Strongly analytic tableaux for normal modal logics.- Reconstructing proofs at the assertion level.- Problems on the generation of finite models.- Combining symbolic computation and theorem proving: Some problems of Ramanujan.- SCOTT: Semantically constrained otter system description.- Protein: A PROver with a Theory Extension INterface.- DELTA — A bottom-up preprocessor for top-down theorem provers.- SETHEO V3.2: Recent developments.- KoMeT.- ?-MKRP: A proof development environment.- LeanT A P: Lean tableau-based theorem proving.- FINDER: Finite domain enumerator system description.- Symlog automated advice in Fitch-style proof construction.- KEIM: A toolkit for automated deduction.- Elf: Ameta-language for deductive systems.- EUODHILOS-II on top of GNU epoch.- Pi: An interactive derivation editor for the calculus of partial inductive definitions.- Mollusc a general proof-development shell for sequent-based logics.- KITP-93: An automated inference system for program analysis.- SPIKE: A system for sufficient completeness and parameterized inductive proofs.- Distributed theorem proving by Peers.