Automated Reasoning with Analytic Tableaux and Related Methods International Conference, TABLEAUX 2000 St Andrews, Scotland, UK, July 3-7, 2000 Proceedings /
Συγγραφή απο Οργανισμό/Αρχή: | |
---|---|
Άλλοι συγγραφείς: | |
Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
Γλώσσα: | 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.