| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996466137003316 |
|
|
Titolo |
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX 2000 St Andrews, Scotland, UK, July 3-7, 2000 Proceedings / / edited by Roy Dyckhoff |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2000.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (X, 440 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Artificial Intelligence ; ; 1847 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Artificial intelligence |
Programming languages (Electronic computers) |
Mathematical logic |
Artificial Intelligence |
Programming Languages, Compilers, Interpreters |
Mathematical Logic and Formal Languages |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references. |
|
|
|
|
|
|
Nota di contenuto |
|
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. |
|
|
|
|
|
| |