Automated Reasoning with Analytic Tableaux and Related Methods International Conference, TABLEAUX 2000 St Andrews, Scotland, UK, July 3-7, 2000 Proceedings /

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Dyckhoff, Roy (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2000.
Έκδοση:1st ed. 2000.
Σειρά:Lecture Notes in Artificial Intelligence ; 1847
Θέματα:
Διαθέσιμο Online:Full Text via HEAL-Link
Πίνακας περιεχομένων:
  • Invited Lectures
  • Tableau Algorithms for Description Logics
  • Modality and Databases
  • Local Symmetries in Propositional Logic
  • Comparison
  • Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison
  • Consistency Testing: The RACE Experience
  • Benchmark Analysis with FaCT
  • MSPASS: Modal Reasoning by Translation and First-Order Resolution
  • TANCS-2000 Results for DLP
  • Evaluating *SAT on TANCS 2000 Benchmarks
  • Research Papers
  • A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations
  • A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus
  • An Analytic Calculus for Quantified Propositional Gödel Logic
  • A Tableau Method for Inconsistency-Adaptive Logics
  • A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning
  • Hypertableau and Path-Hypertableau Calculi for some Families of Intermediate Logics
  • Variants of First-Order Modal Logics
  • Complexity of Simple Dependent Bimodal Logics
  • Properties of Embeddings from Int to S4
  • Term-Modal Logics
  • A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics
  • Dual Intuitionistic Logic Revisited
  • Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions
  • Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints
  • Matrix-Based Inductive Theorem Proving
  • Monotonic Preorders for Free Variable Tableaux
  • The Mosaic Method for Temporal Logics
  • Sequent-Like Tableau Systems with the Analytic Superformula Property for the Modal Logics KB, KDB, K5, KD5
  • A Tableau Calculus for Equilibrium Entailment
  • Towards Tableau-Based Decision Procedures for Non-Well-Founded Fragments of Set Theory
  • Tableau Calculus for Only Knowing and Knowing At Most
  • A Tableau-Like Representation Framework for Efficient Proof Reconstruction
  • The Semantic Tableaux Version of the Second Incompleteness Theorem Extends Almost to Robinson's Arithmetic Q
  • System Descriptions
  • Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO
  • E-SETHEO: An Automated3 Theorem Prover.