Automated Reasoning First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings /

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Gore, Rajeev (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Leitsch, Alexander (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Nipkow, Tobias (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2001.
Έκδοση:1st ed. 2001.
Σειρά:Lecture Notes in Artificial Intelligence ; 2083
Θέματα:
Διαθέσιμο Online:Full Text via HEAL-Link
Πίνακας περιεχομένων:
  • Invited Talks
  • Program Termination Analysis by Size-Change 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
  • NExpTime-Complete 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
  • Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL
  • Deduction-Based 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
  • Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation
  • Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation
  • Saturation Based Theorem Proving, Applications, and Data Structures
  • Instructing Equational Set-Reasoning with Otter
  • NP-Completeness of Refutability by Literal-Once Resolution
  • Ordered Resolution vs. Connection Graph resolution
  • A Model-Based Completeness Proof of Extended Narrowing and Resolution
  • A Model-Based Completeness Proof of Extended Narrowing and Resolution
  • A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality
  • A Resolution-Based Decision Procedure for the Two-Variable 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 Top-Down Procedure for Disjunctive Well-Founded Semantics
  • A Second-Order Theorem Prover Applied to Circumscription
  • NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics
  • NoMoRe: A System for Non-Monotonic 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, Higher-Order Logic, Interactive Theorem Proving
  • More On Implicit Syntax
  • Termination and Reduction Checking for Higher-Order Logic Programs
  • P.rex: An Interactive Proof Explainer
  • JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants
  • Semantic Guidance
  • The eXtended Least Number Heuristic
  • System Description: SCOTT-5
  • Combination of Distributed Search and Multi-Search in Peers-mcd.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 Meta-Complexity Theorem for Bottom-Up Logic Programs
  • Tableau, Sequent, Natural Deduction Calculi and Proof Theory
  • Canonical Propositional Gentzen-Type 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 First-Order 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 Connection-Method Theorem Prover for First-Order Classical Logic
  • Nonclassical Logics
  • Muscadet 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction
  • Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory
  • STRIP: Structural Sharing for Efficient Proof-Search
  • RACER System Description.