| Description |
1 online resource : illustrations (some color) |
| Series |
Lecture notes in artificial intelligence ; 11714 |
|
LNCS sublibrary. SL 7, Artificial intelligence |
|
Lecture notes in computer science ; 11714.
|
|
Lecture notes in computer science. Lecture notes in artificial intelligence.
|
|
LNCS sublibrary. SL 7, Artificial intelligence.
|
| Contents |
Intro; Preface; Organization; Abstracts of Invited Talks; Automated Reasoning for the Working Mathematician; Remembering Roy Dyckhoff; Contents; Tableau Calculi; A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL; 1 Introduction; 2 Preliminaries; 2.1 Linear Temporal Logic; 2.2 The One-Pass and Tree-Shaped Tableau System; 3 SAT-Based Encoding of the Tableau; 3.1 Notation; 3.2 Expansion of the Tree; 3.3 Encoding of Accepted Branches; 4 Completeness; 5 Experimental Evaluation; 6 Conclusions; References; Certification of Nonclausal Connection Tableaux Proofs |
|
1 Introduction2 Connection Calculi; 3 Compressed Connection Calculi; 4 Connection Proof Translation; 4.1 Clausal Proof Translation; 4.2 Nonclausal Proof Translation; 5 Implementation; 6 Evaluation; 7 Related Work; 8 Conclusion; References; Preferential Tableaux for Contextual Defeasible ALC; 1 Introduction; 2 Logical Preliminaries; 3 Contextual Defeasible ALC; 4 Tableau for Preferential Reasoning in dALC; 5 Related Work; 6 Concluding Remarks; References; A Tableau Calculus for Non-clausal Maximum Satisfiability; 1 Introduction; 2 Background; 3 A Non-clausal MaxSAT Tableau Calculus |
|
3.1 Soundness and Completeness4 Extension to Hard and Weighted Formulas; 5 Conclusions; References; Sequent Calculi; First-Order Quasi-canonical Proof Systems; 1 Introduction; 2 Preliminaries; 3 Quasi-canonical Systems; 3.1 Introducing Quasi-canonical Proof Systems; 3.2 The Semantics of Quasi-canonical Proof Systems; 3.3 Soundness, Completeness, and Cut-Elimination; 4 Existential Information Processing; 4.1 Sources of Information; 4.2 Gathering and Processing the Information; 4.3 Proof System for Processors; 5 Conclusion and Future Research; References |
|
Bounded Sequent Calculi for Non-classical Logics via Hypersequents1 Introduction; 2 Preliminaries; 3 A Guided Example Demonstrating the Methodology; 4 The Disjunction Form of a Rule: A Formal Definition; 5 Disjunction Forms for Commutative Substructural Logics; 6 Bounded Calculi for Commutative Substructural Logics; 6.1 Application: Decidability and Complexity Of FLecm Extensions; 7 The Methodology Applied to Modal Logics; References; A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic; 1 Introduction; 2 Syntax and Kripke Semantics of IPL |
|
3 The Theorem Prover intuit3.1 intuit in Detail; 4 Adapting the Sequent Calculus LJT to Clausal Forms; 4.1 Root-First Proof Search, Invertibility and Recursivity; 4.2 LJT Specialised to Clausal Forms; 4.3 A Generalised Version of (L); 5 The Calculus LJTSAT; 6 Proof-Search Using LJTSAT; 7 Discussion, Further Work and Conclusions; References; Relating Labelled and Label-Free Bunched Calculi in BI Logic; 1 Introduction; 2 The Logic BI; 2.1 Syntax and Sequent Calculus LBI; 2.2 Semantics of BI; 3 The Labelled Calculus GBI; 3.1 Soundness of GBI; 4 From LBI-Proofs to GBI-Proofs |
| Summary |
This book constitutes the proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019, held in London, UK, in September 2019, colocated with the 12th International Symposium on Frontiers on Combining Systems, FroCoS 2019. The 25 full papers presented were carefully reviewed and selected from 43 submissions. They present research on all aspects of the mechanization of tableaux-based reasoning and related methods, including theoretical foundations, implementation techniques, systems development and applications. The papers are organized in the following topical sections: tableau calculi, sequent calculi, semantics and combinatorial proofs, non-wellfounded proof systems, automated theorem provers, and logics for program or system verification |
| Bibliography |
Includes bibliographical references and index |
| Notes |
Online resource; title from PDF title page (SpringerLink, viewed September 11, 2019) |
| Subject |
Automatic theorem proving -- Congresses
|
|
Automatic theorem proving
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Cerrito, Serenella, editor
|
|
Popescu, Andrei, editor
|
| ISBN |
9783030290269 |
|
3030290263 |
|
3030290255 |
|
9783030290252 |
|
9783030290276 |
|
3030290271 |
|
