Borrow it
 Architecture Library
 Bizzell Memorial Library
 Boorstin Collection
 Chinese Literature Translation Archive
 Engineering Library
 Fine Arts Library
 Harry W. Bass Business History Collection
 History of Science Collections
 John and Mary Nichols Rare Books and Special Collections
 Library Service Center
 Price College Digital Library
 Western History Collections
The Resource Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource)
Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource)
Resource Information
The item Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Oklahoma Libraries.This item is available to borrow from all library branches.
Resource Information
The item Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Oklahoma Libraries.
This item is available to borrow from all library branches.
 Summary
 This book constitutes the refereed proceedings of the First International Joint Conference on Automated Reasoning, IJCAR 2001, held in Siena, Italy, in June 2001. The 37 research papers and 19 system descriptions presented together with three invited contributions were carefully reviewed and selected from a total of 112 submissions. The book offers topical sections on description, modal, and temporal logics; saturation based theorem proving, applications, and data structures; logic programming and nonmonotonic reasoning; propositional satisfiability and quantified Boolean logic; logical frameworks, higherorder logic, and interactive theorem proving; equational theorem proving and term rewriting; tableau, sequent, and natural deduction calculi and proof theory; automata, specification, verification, and logics of programs; and nonclassical logics
 Language
 eng
 Extent
 1 online resource.
 Contents

 Invited Talks
 Program Termination Analysis by SizeChange Graphs (Abstract)
 SET Cardholder Registration: The Secrecy Proofs
 SET Cardholder Registration: The Secrecy Proofs
 Algorithms, Datastructures, and other Issues in Efficient Automated Deduction
 Algorithms, Datastructures, and other Issues in Efficient Automated Deduction
 Description, Modal and temporal Logics
 The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach
 NExpTimeComplete Description Logics with Concrete Domains
 Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics
 Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics
 The Hybrid ?Calculus
 The Hybrid ?Calculus
 The Inverse Method Implements the Automata Approach for Modal Satisfiability
 The Inverse Method Implements the Automata Approach for Modal Satisfiability
 DeductionBased Decision Procedure for a Clausal Miniscoped Fragment of FTL
 DeductionBased Decision Procedure for a Clausal Miniscoped Fragment of FTL
 Tableaux for Temporal Description Logic with Constant Domains
 Tableaux for Temporal Description Logic with Constant Domains
 FreeVariable Tableaux for ConstantDomain Quantified Modal Logics with Rigid and Nonrigid Designation
 FreeVariable Tableaux for ConstantDomain Quantified Modal Logics with Rigid and Nonrigid Designation
 Saturation Based Theorem Proving, Applications, and Data Structures
 Instructing Equational SetReasoning with Otter
 NPCompleteness of Refutability by LiteralOnce Resolution
 Ordered Resolution vs. Connection Graph resolution
 A ModelBased Completeness Proof of Extended Narrowing and Resolution
 A ModelBased Completeness Proof of Extended Narrowing and Resolution
 A ResolutionBased Decision Procedure for the TwoVariable Fragment with Equality
 A ResolutionBased Decision Procedure for the TwoVariable Fragment with Equality
 Superposition and Chaining for Totally Ordered Divisible Abelian Groups
 Superposition and Chaining for Totally Ordered Divisible Abelian Groups
 Context Trees
 Context Trees
 On the Evaluation of Indexing Techniques for Theorem Proving
 On the Evaluation of Indexing Techniques for Theorem Proving
 Logic Programming and Nonmonotonic Reasoning
 Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation
 Bunched Logic Programming
 A TopDown Procedure for Disjunctive WellFounded Semantics
 A SecondOrder Theorem Prover Applied to Circumscription
 NoMoRe: A System for NonMonotonic Reasoning with Logic Programs under Answer Set Semantics
 NoMoRe: A System for NonMonotonic Reasoning with Logic Programs under Answer Set Semantics
 Propositional Satisfiability and Quantified Boolean Logic
 Conditional Pure Literal Graphs
 Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability
 QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability
 System Abstract: E 0.61
 Vampire 1.1
 DCTP
 A Disconnection Calculus Theorem Prover
 System Abstract
 DCTP
 A Disconnection Calculus Theorem Prover
 System Abstract
 Logical Frameworks, HigherOrder Logic, Interactive Theorem Proving
 More On Implicit Syntax
 Termination and Reduction Checking for HigherOrder Logic Programs
 P.rex: An Interactive Proof Explainer
 JProver: Integrating ConnectionBased Theorem Proving into Interactive Proof Assistants
 Semantic Guidance
 The eXtended Least Number Heuristic
 System Description: SCOTT5
 Combination of Distributed Search and MultiSearch in Peersmcd.d
 Lotrec: The Generic Tableau Prover for Modal and Description Logics
 The modprof Theorem Prover
 A New System and Methodology for Generating Random Modal Formulae
 Equational Theorem Proving and Term Rewriting
 Decidable Classes of Inductive Theorems
 Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems
 Decidability and Complexity of Finitely Closable Linear Equational Theories
 A New MetaComplexity Theorem for BottomUp Logic Programs
 Tableau, Sequent, Natural Deduction Calculi and Proof Theory
 Canonical Propositional GentzenType Systems
 Incremental Closure of Free Variable Tableaux
 Deriving Modular Programs from Short Proofs
 A General Method for Using Schematizations in Automated Deduction
 Automata, Specification, Verification, and Logics of Programs
 Approximating Dependency Graphs Using Tree Automata Techniques
 On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables
 A Sequent Calculus for FirstOrder Dynamic Logic with Trace Modalities
 Flaw Detection in Formal Specifications
 CCE: Testing Ground Joinability
 System Description: RDL Rewrite and Decision Procedure Laboratory
 lolliCoP
 A Linear Logic Implementation of a Lean ConnectionMethod Theorem Prover for FirstOrder Classical Logic
 Nonclassical Logics
 Muscadet 2.3: A KnowledgeBased Theorem Prover Based on Natural Deduction
 Hilberticus
 A Tool Deciding an Elementary Sublanguage of Set Theory
 STRIP: Structural Sharing for Efficient ProofSearch
 RACER System Description
 Isbn
 9783540457442
 Label
 Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings
 Title
 Automated Reasoning
 Title remainder
 First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings
 Statement of responsibility
 edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow
 Language
 eng
 Summary
 This book constitutes the refereed proceedings of the First International Joint Conference on Automated Reasoning, IJCAR 2001, held in Siena, Italy, in June 2001. The 37 research papers and 19 system descriptions presented together with three invited contributions were carefully reviewed and selected from a total of 112 submissions. The book offers topical sections on description, modal, and temporal logics; saturation based theorem proving, applications, and data structures; logic programming and nonmonotonic reasoning; propositional satisfiability and quantified Boolean logic; logical frameworks, higherorder logic, and interactive theorem proving; equational theorem proving and term rewriting; tableau, sequent, and natural deduction calculi and proof theory; automata, specification, verification, and logics of programs; and nonclassical logics
 Cataloging source
 DKDLA
 Dewey number
 006.3
 Index
 no index present
 LC call number
 QA76.9.A96 I38 2001
 Literary form
 non fiction
 Nature of contents

 dictionaries
 standards specifications
 http://library.link/vocab/relatedWorkOrContributorName

 Gor Rajeev
 Leitsch, Alexander
 Nipkow, Tobias
 Series statement
 Lecture Notes in Computer Science
 Series volume
 2083,
 http://library.link/vocab/subjectName

 Computer science
 Software engineering
 Logic design
 Artificial intelligence
 Logic, Symbolic and mathematical
 Artificial Intelligence (incl. Robotics)
 Mathematical Logic and Formal Languages
 Logics and Meanings of Programs
 Mathematical Logic and Foundations
 Label
 Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource)
 Contents
 Invited Talks  Program Termination Analysis by SizeChange Graphs (Abstract)  SET Cardholder Registration: The Secrecy Proofs  SET Cardholder Registration: The Secrecy Proofs  Algorithms, Datastructures, and other Issues in Efficient Automated Deduction  Algorithms, Datastructures, and other Issues in Efficient Automated Deduction  Description, Modal and temporal Logics  The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach  NExpTimeComplete Description Logics with Concrete Domains  Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics  Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics  The Hybrid ?Calculus  The Hybrid ?Calculus  The Inverse Method Implements the Automata Approach for Modal Satisfiability  The Inverse Method Implements the Automata Approach for Modal Satisfiability  DeductionBased Decision Procedure for a Clausal Miniscoped Fragment of FTL  DeductionBased Decision Procedure for a Clausal Miniscoped Fragment of FTL  Tableaux for Temporal Description Logic with Constant Domains  Tableaux for Temporal Description Logic with Constant Domains  FreeVariable Tableaux for ConstantDomain Quantified Modal Logics with Rigid and Nonrigid Designation  FreeVariable Tableaux for ConstantDomain Quantified Modal Logics with Rigid and Nonrigid Designation  Saturation Based Theorem Proving, Applications, and Data Structures  Instructing Equational SetReasoning with Otter  NPCompleteness of Refutability by LiteralOnce Resolution  Ordered Resolution vs. Connection Graph resolution  A ModelBased Completeness Proof of Extended Narrowing and Resolution  A ModelBased Completeness Proof of Extended Narrowing and Resolution  A ResolutionBased Decision Procedure for the TwoVariable Fragment with Equality  A ResolutionBased Decision Procedure for the TwoVariable Fragment with Equality  Superposition and Chaining for Totally Ordered Divisible Abelian Groups  Superposition and Chaining for Totally Ordered Divisible Abelian Groups  Context Trees  Context Trees  On the Evaluation of Indexing Techniques for Theorem Proving  On the Evaluation of Indexing Techniques for Theorem Proving  Logic Programming and Nonmonotonic Reasoning  Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation  Bunched Logic Programming  A TopDown Procedure for Disjunctive WellFounded Semantics  A SecondOrder Theorem Prover Applied to Circumscription  NoMoRe: A System for NonMonotonic Reasoning with Logic Programs under Answer Set Semantics  NoMoRe: A System for NonMonotonic Reasoning with Logic Programs under Answer Set Semantics  Propositional Satisfiability and Quantified Boolean Logic  Conditional Pure Literal Graphs  Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability  QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability  System Abstract: E 0.61  Vampire 1.1  DCTP  A Disconnection Calculus Theorem Prover  System Abstract  DCTP  A Disconnection Calculus Theorem Prover  System Abstract  Logical Frameworks, HigherOrder Logic, Interactive Theorem Proving  More On Implicit Syntax  Termination and Reduction Checking for HigherOrder Logic Programs  P.rex: An Interactive Proof Explainer  JProver: Integrating ConnectionBased Theorem Proving into Interactive Proof Assistants  Semantic Guidance  The eXtended Least Number Heuristic  System Description: SCOTT5  Combination of Distributed Search and MultiSearch in Peersmcd.d  Lotrec: The Generic Tableau Prover for Modal and Description Logics  The modprof Theorem Prover  A New System and Methodology for Generating Random Modal Formulae  Equational Theorem Proving and Term Rewriting  Decidable Classes of Inductive Theorems  Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems  Decidability and Complexity of Finitely Closable Linear Equational Theories  A New MetaComplexity Theorem for BottomUp Logic Programs  Tableau, Sequent, Natural Deduction Calculi and Proof Theory  Canonical Propositional GentzenType Systems  Incremental Closure of Free Variable Tableaux  Deriving Modular Programs from Short Proofs  A General Method for Using Schematizations in Automated Deduction  Automata, Specification, Verification, and Logics of Programs  Approximating Dependency Graphs Using Tree Automata Techniques  On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables  A Sequent Calculus for FirstOrder Dynamic Logic with Trace Modalities  Flaw Detection in Formal Specifications  CCE: Testing Ground Joinability  System Description: RDL Rewrite and Decision Procedure Laboratory  lolliCoP  A Linear Logic Implementation of a Lean ConnectionMethod Theorem Prover for FirstOrder Classical Logic  Nonclassical Logics  Muscadet 2.3: A KnowledgeBased Theorem Prover Based on Natural Deduction  Hilberticus  A Tool Deciding an Elementary Sublanguage of Set Theory  STRIP: Structural Sharing for Efficient ProofSearch  RACER System Description
 Extent
 1 online resource.
 Form of item
 online
 Governing access note
 Online full text is restricted to subscribers
 Isbn
 9783540457442
 Isbn Type
 (electronic bk.)
 Specific material designation
 remote
 System control number

 (OCoLC)768058484
 (OCoLC)ocn768058484
 Label
 Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource)
 Contents
 Invited Talks  Program Termination Analysis by SizeChange Graphs (Abstract)  SET Cardholder Registration: The Secrecy Proofs  SET Cardholder Registration: The Secrecy Proofs  Algorithms, Datastructures, and other Issues in Efficient Automated Deduction  Algorithms, Datastructures, and other Issues in Efficient Automated Deduction  Description, Modal and temporal Logics  The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach  NExpTimeComplete Description Logics with Concrete Domains  Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics  Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics  The Hybrid ?Calculus  The Hybrid ?Calculus  The Inverse Method Implements the Automata Approach for Modal Satisfiability  The Inverse Method Implements the Automata Approach for Modal Satisfiability  DeductionBased Decision Procedure for a Clausal Miniscoped Fragment of FTL  DeductionBased Decision Procedure for a Clausal Miniscoped Fragment of FTL  Tableaux for Temporal Description Logic with Constant Domains  Tableaux for Temporal Description Logic with Constant Domains  FreeVariable Tableaux for ConstantDomain Quantified Modal Logics with Rigid and Nonrigid Designation  FreeVariable Tableaux for ConstantDomain Quantified Modal Logics with Rigid and Nonrigid Designation  Saturation Based Theorem Proving, Applications, and Data Structures  Instructing Equational SetReasoning with Otter  NPCompleteness of Refutability by LiteralOnce Resolution  Ordered Resolution vs. Connection Graph resolution  A ModelBased Completeness Proof of Extended Narrowing and Resolution  A ModelBased Completeness Proof of Extended Narrowing and Resolution  A ResolutionBased Decision Procedure for the TwoVariable Fragment with Equality  A ResolutionBased Decision Procedure for the TwoVariable Fragment with Equality  Superposition and Chaining for Totally Ordered Divisible Abelian Groups  Superposition and Chaining for Totally Ordered Divisible Abelian Groups  Context Trees  Context Trees  On the Evaluation of Indexing Techniques for Theorem Proving  On the Evaluation of Indexing Techniques for Theorem Proving  Logic Programming and Nonmonotonic Reasoning  Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation  Bunched Logic Programming  A TopDown Procedure for Disjunctive WellFounded Semantics  A SecondOrder Theorem Prover Applied to Circumscription  NoMoRe: A System for NonMonotonic Reasoning with Logic Programs under Answer Set Semantics  NoMoRe: A System for NonMonotonic Reasoning with Logic Programs under Answer Set Semantics  Propositional Satisfiability and Quantified Boolean Logic  Conditional Pure Literal Graphs  Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability  QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability  System Abstract: E 0.61  Vampire 1.1  DCTP  A Disconnection Calculus Theorem Prover  System Abstract  DCTP  A Disconnection Calculus Theorem Prover  System Abstract  Logical Frameworks, HigherOrder Logic, Interactive Theorem Proving  More On Implicit Syntax  Termination and Reduction Checking for HigherOrder Logic Programs  P.rex: An Interactive Proof Explainer  JProver: Integrating ConnectionBased Theorem Proving into Interactive Proof Assistants  Semantic Guidance  The eXtended Least Number Heuristic  System Description: SCOTT5  Combination of Distributed Search and MultiSearch in Peersmcd.d  Lotrec: The Generic Tableau Prover for Modal and Description Logics  The modprof Theorem Prover  A New System and Methodology for Generating Random Modal Formulae  Equational Theorem Proving and Term Rewriting  Decidable Classes of Inductive Theorems  Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems  Decidability and Complexity of Finitely Closable Linear Equational Theories  A New MetaComplexity Theorem for BottomUp Logic Programs  Tableau, Sequent, Natural Deduction Calculi and Proof Theory  Canonical Propositional GentzenType Systems  Incremental Closure of Free Variable Tableaux  Deriving Modular Programs from Short Proofs  A General Method for Using Schematizations in Automated Deduction  Automata, Specification, Verification, and Logics of Programs  Approximating Dependency Graphs Using Tree Automata Techniques  On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables  A Sequent Calculus for FirstOrder Dynamic Logic with Trace Modalities  Flaw Detection in Formal Specifications  CCE: Testing Ground Joinability  System Description: RDL Rewrite and Decision Procedure Laboratory  lolliCoP  A Linear Logic Implementation of a Lean ConnectionMethod Theorem Prover for FirstOrder Classical Logic  Nonclassical Logics  Muscadet 2.3: A KnowledgeBased Theorem Prover Based on Natural Deduction  Hilberticus  A Tool Deciding an Elementary Sublanguage of Set Theory  STRIP: Structural Sharing for Efficient ProofSearch  RACER System Description
 Extent
 1 online resource.
 Form of item
 online
 Governing access note
 Online full text is restricted to subscribers
 Isbn
 9783540457442
 Isbn Type
 (electronic bk.)
 Specific material designation
 remote
 System control number

 (OCoLC)768058484
 (OCoLC)ocn768058484
Library Locations

Architecture LibraryBorrow itGould Hall 830 Van Vleet Oval Rm. 105, Norman, OK, 73019, US35.205706 97.445050



Chinese Literature Translation ArchiveBorrow it401 W. Brooks St., RM 414, Norman, OK, 73019, US35.207487 97.447906

Engineering LibraryBorrow itFelgar Hall 865 Asp Avenue, Rm. 222, Norman, OK, 73019, US35.205706 97.445050

Fine Arts LibraryBorrow itCatlett Music Center 500 West Boyd Street, Rm. 20, Norman, OK, 73019, US35.210371 97.448244

Harry W. Bass Business History CollectionBorrow it401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US35.207487 97.447906

History of Science CollectionsBorrow it401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US35.207487 97.447906

John and Mary Nichols Rare Books and Special CollectionsBorrow it401 W. Brooks St., Rm. 509NW, Norman, OK, 73019, US35.207487 97.447906


Price College Digital LibraryBorrow itAdams Hall 102 307 West Brooks St., Norman, OK, 73019, US35.210371 97.448244

Western History CollectionsBorrow itMonnet Hall 630 Parrington Oval, Rm. 300, Norman, OK, 73019, US35.209584 97.445414
Embed (Experimental)
Settings
Select options that apply then copy and paste the RDF/HTML data fragment to include in your application
Embed this data in a secure (HTTPS) page:
Layout options:
Include data citation:
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.libraries.ou.edu/portal/AutomatedReasoningFirstInternationalJoint/coDDzJ5fjnM/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.libraries.ou.edu/portal/AutomatedReasoningFirstInternationalJoint/coDDzJ5fjnM/">Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.libraries.ou.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.libraries.ou.edu/">University of Oklahoma Libraries</a></span></span></span></span></div>
Note: Adjust the width and height settings defined in the RDF/HTML code fragment to best match your requirements
Preview
Cite Data  Experimental
Data Citation of the Item Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource)
Copy and paste the following RDF/HTML data fragment to cite this resource
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.libraries.ou.edu/portal/AutomatedReasoningFirstInternationalJoint/coDDzJ5fjnM/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.libraries.ou.edu/portal/AutomatedReasoningFirstInternationalJoint/coDDzJ5fjnM/">Automated Reasoning : First International Joint Conference, IJCAR 2001 Siena, Italy, June 1822, 2001 Proceedings, edited by Rajeev Gor, Alexander Leitsch, Tobias Nipkow, (electronic resource)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.libraries.ou.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.libraries.ou.edu/">University of Oklahoma Libraries</a></span></span></span></span></div>