Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
Filter
Type of Material
Type of Publication
Consortium
Language
  • 1
    UID:
    (DE-604)BV021986064
    Format: III, 57 Bl.
    Note: 1niversity Park, Pa., Univ., Diss., 1974. -Kopie, erschienen im Verl. Univ. Microfilms Internat., Ann Arbor, Mich.
    Language: English
    Keywords: Hochschulschrift
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 2
    UID:
    (DE-602)almafu_9959186269802883
    Format: 1 online resource (X, 776 p.)
    Edition: 1st ed. 1988.
    Edition: Online edition Springer Lecture Notes Archive ; 041142-5
    ISBN: 3-540-39216-5
    Series Statement: Lecture Notes in Computer Science, 310
    Content: This volume contains the papers presented at the Ninth International Conference on Automated Deduction (CADE-9) held May 23-26 at Argonne National Laboratory, Argonne, Illinois. The conference commemorates the twenty-fifth anniversary of the discovery of the resolution principle, which took place during the summer of 1963. The CADE conferences are a forum for reporting on research on all aspects of automated deduction, including theorem proving, logic programming, unification, deductive databases, term rewriting, ATP for non-standard logics, and program verification. All papers submitted to the conference were refereed by at least two referees, and the program committee accepted the 52 that appear here. Also included in this volume are abstracts of 21 implementations of automated deduction systems.
    Note: Bibliographic Level Mode of Issuance: Monograph , 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 for situations -- 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. , English
    In: Springer eBooks
    Additional Edition: ISBN 3-540-19343-X
    Language: English
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 3
    UID:
    (DE-602)edoccha_9959186269802883
    Format: 1 online resource (X, 776 p.)
    Edition: 1st ed. 1988.
    Edition: Online edition Springer Lecture Notes Archive ; 041142-5
    ISBN: 3-540-39216-5
    Series Statement: Lecture Notes in Computer Science, 310
    Content: This volume contains the papers presented at the Ninth International Conference on Automated Deduction (CADE-9) held May 23-26 at Argonne National Laboratory, Argonne, Illinois. The conference commemorates the twenty-fifth anniversary of the discovery of the resolution principle, which took place during the summer of 1963. The CADE conferences are a forum for reporting on research on all aspects of automated deduction, including theorem proving, logic programming, unification, deductive databases, term rewriting, ATP for non-standard logics, and program verification. All papers submitted to the conference were refereed by at least two referees, and the program committee accepted the 52 that appear here. Also included in this volume are abstracts of 21 implementations of automated deduction systems.
    Note: Bibliographic Level Mode of Issuance: Monograph , 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 for situations -- 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. , English
    In: Springer eBooks
    Additional Edition: ISBN 3-540-19343-X
    Language: English
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 4
    UID:
    (DE-605)HT021189481
    Format: 1 Online-Ressource (X, 776 p)
    Edition: 1st ed. 1988
    ISBN: 9783540392163
    Series Statement: Lecture Notes in Computer Science 310
    Additional Edition: Printed edition 9783662167793
    Additional Edition: Printed edition 9783540193432
    Language: English
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 5
    UID:
    (DE-602)edocfu_9959186269802883
    Format: 1 online resource (X, 776 p.)
    Edition: 1st ed. 1988.
    Edition: Online edition Springer Lecture Notes Archive ; 041142-5
    ISBN: 3-540-39216-5
    Series Statement: Lecture Notes in Computer Science, 310
    Content: This volume contains the papers presented at the Ninth International Conference on Automated Deduction (CADE-9) held May 23-26 at Argonne National Laboratory, Argonne, Illinois. The conference commemorates the twenty-fifth anniversary of the discovery of the resolution principle, which took place during the summer of 1963. The CADE conferences are a forum for reporting on research on all aspects of automated deduction, including theorem proving, logic programming, unification, deductive databases, term rewriting, ATP for non-standard logics, and program verification. All papers submitted to the conference were refereed by at least two referees, and the program committee accepted the 52 that appear here. Also included in this volume are abstracts of 21 implementations of automated deduction systems.
    Note: Bibliographic Level Mode of Issuance: Monograph , 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 for situations -- 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. , English
    In: Springer eBooks
    Additional Edition: ISBN 3-540-19343-X
    Language: English
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 6
    Online Resource
    Online Resource
    Berlin, Heidelberg : Springer Berlin Heidelberg
    UID:
    (DE-602)gbv_1649209363
    Format: Online-Ressource
    ISBN: 9783540392163
    Series Statement: Lecture Notes in Computer Science 310
    Additional Edition: ISBN 9783540193432
    Additional Edition: Buchausg. u.d.T. Argonne, Illinois, USA, May 23 - 26, 1988 1988 ISBN 354019343X
    Additional Edition: ISBN 038719343X
    Language: English
    Subjects: Computer Science
    RVK:
    URL: Cover
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 7
    Online Resource
    Online Resource
    Berlin, Heidelberg : Springer Berlin Heidelberg
    UID:
    (DE-627)1649209363
    Format: Online-Ressource
    ISBN: 9783540392163
    Series Statement: Lecture Notes in Computer Science 310
    Additional Edition: 9783540193432
    Additional Edition: Buchausg. u.d.T. Argonne, Illinois, USA, May 23 - 26, 1988 1988 354019343X
    Additional Edition: 038719343X
    Language: English
    Subjects: Computer Science
    RVK:
    URL: Cover
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 8
    UID:
    (DE-603)28764524X
    Format: ... S.
    Edition: Online-Ausg. Berlin [u.a.] Springer 2011 Online-Ressource SpringerLink: Springer e-Books ISBN 9783540392163
    Edition: ISBN 3540392165
    Edition: Online-Ausg.
    ISBN: 9783540193432 , 354019343X , 9783540392163 (Sekundärausgabe) , 3540392165 (Sekundärausgabe)
    Series Statement: Lecture Notes in Computer Science 310
    Note: Online-Ausg.:
    Language: English
    Subjects: Computer Science
    RVK:
    Keywords: Online-Publikation
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 9
    UID:
    (DE-605)HT017814751
    Edition: Springer Lecture Notes Archive IDNR 041142-5
    ISBN: 9783540193432 , 9783540392163
    Note: Sofern kein Zugang über ein Universitätsnetz zur Verfügung steht, kann eine Registrierung zur kostenlosen Nutzung erfolgen: http://www.nationallizenzen.de
    Additional Information: In ---〉 Springer eBooks
    Language: English
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 10
    Book
    Book
    CHICAGO : Science Research Assoc.
    UID:
    (DE-605)HT000747917
    Format: X,372 S.
    ISBN: 0574210857
    Language: Undetermined
    Subjects: Computer Science , Economics
    RVK:
    RVK:
    Keywords: Assembler ; ASSIST
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
Close ⊗
This website uses cookies and the analysis tool Matomo. Further information can be found on the KOBV privacy pages