Automated Reasoning with Analytic Tableaux and Related Methods

Name: Automated Reasoning with Analytic Tableaux and Related Methods | 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings

Serenella Cerrito Andrei Popescu(Editor)

Springer (Publisher)

Published on 22. August 2019

XXI, 477 pages

E-Book

PDF with digital watermarking

System requirements

978-3-030-29026-9 (ISBN)

€53.49incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

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 Introduction
2 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 Completeness
4 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 Hypersequents
1 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 intuit
3.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
5 Back from GBI-Proofs to LBI-Proofs
6 Conclusion and Future Work
References
Sequentialising Nested Systems
1 Introduction
2 Sequent Systems
3 Nested Systems
3.1 Normal Forms in NS
4 Recovering Sequent Systems
5 Examples and Discussion
6 Conclusion and Future Work
References
A Hypersequent Calculus with Clusters for Data Logic over Ordinals
1 Introduction
2 Freeze Tense Logic over Ordinals
3 Hypersequents with Clusters
3.1 Syntax
3.2 Semantics
4 Proof System
4.1 Notations
4.2 Rules
4.3 Soundness
5 Restricted Logic and Completeness
5.1 Restricted Syntax
5.2 Completeness and Complexity
6 Restricted Logic on Given Ordinals
7 Related Work and Conclusion
References
Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents
1 Introduction
2 Preliminaries
3 A Linear Nested Sequent Calculus for Kt
4 Completeness via Proof Search and Counter-Models
4.1 Pruning Irrelevant Branches from the Search Space
5 Completeness via Cut Elimination
6 Application: Linear Nested Sequents for Modal Logic KB
7 Conclusion
References
Combining Monotone and Normal Modal Logic in Nested Sequents - with Countermodels
1 Introduction
2 The Basic System
3 Cut Elimination
4 Completeness via Countermodel Generation
5 Extensions
6 Implementation
7 Conclusion
References
Semantics and Combinatorial Proofs
On Combinatorial Proofs for Modal Logic
1 Introduction
2 Sequent Calculus
3 Relation Webs
4 RGB-Cographs and Linear Proofs for K and KD
5 Skew Fibrations
6 Combinatorial Proofs for the Modal Logics K and D
7 Combinatorial Proofs for the Logics in the S4-plane
8 Non-normal Modal Logics
9 Conclusion and Future Work
References
A Game Model for Proofs with Costs
1 Introduction
2 A Game Model of Branching
3 Adding Costs
3.1 The Spectrum of a Provable Sequent
3.2 Cut Admissibility
4 Alternative Cost Structures
5 Modalities in Positive Contexts
6 Concluding Remarks and Future Work
References
Towards a Combinatorial Proof Theory
1 Introduction
2 Formulas and Cographs
3 Combinatorial Proofs
4 Open Deduction
5 Homomorphisms Classes and Structural Proof Systems
6 Basic Correspondences
7 Restricting c"3223379 or w"3223379 : Affine and Relevance Logic
8 Restricting to Shallow Inference: A Logic of Fibrations
9 Conclusion
References
Birkhoff Completeness for Hybrid-Dynamic First-Order Logic
1 Introduction
2 Hybrid-Dynamic First-Order Logic
3 Entailment
4 Atomic Completeness
5 Quasi-completeness
6 Horn-Clause Completeness
7 Conclusions
References
Non-Wellfounded Proof Systems
Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory
1 Introduction
2 Background
3 A First Taste of Proof-Nets in Logics with Fixed Points
4 Infinets
5 Correctness Criteria
6 Sequentialization
7 Canonicity
8 Cut Elimination
9 Conclusion
References
PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest Fixed Points
1 Introduction
2 Background on Circular Proofs and Thread Validity
2.1 Formulas
2.2 Sequents and Preproofs
2.3 Proofs
2.4 Deciding Thread Validity in PSPACE
3 PSPACE-Completeness
3.1 Outline of the PSPACE-Completeness Proof
3.2 Defining the Reduction
3.3 Main Theorem
4 Comments on Our Approach and Discussion of Related Works
5 Conclusion
References
A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
1 Introduction
2 PDL: Syntax and Semantics
3 An Infinitary, Labelled Sequent Calculus
4 Completeness
4.1 Cut-Free Completeness of G3PDL
4.2 Completeness of G3PDL for PDL
5 Proof Search for Test-Free, Acyclic Sequents
6 Conclusion
References
Automated Theorem Provers
Herbrand Constructivization for Automated Intuitionistic Theorem Proving
1 Introduction
2 Overview of the Prover
3 Expansion Proofs
4 Proof Constructivization
5 Optimizations
6 Completeness on Subclasses
7 Experimental Evaluation
8 Conclusion
References
ENIGMAWatch: ProofWatch Meets ENIGMA
1 Introduction
2 Guiding the Given Clause Selection in ATPs
2.1 Automated Theorem Proving and Machine Learning
2.2 ENIGMA: Learning from Successful Proof Searches
2.3 ProofWatch: Proof Guidance by Clause Subsumption
3 ENIGMAWatch: ProofWatch Meets ENIGMA
3.1 Completion Ratios as Semantic Embeddings of the Proof Search
3.2 Proof Vector Construction
4 Multi-indices Subsumption Indexing
5 Experiments
5.1 Multi-indices Subsumption Indexing Evaluation
5.2 Experimental Evaluation of ENIGMAWatch
5.3 Training, Model Statistics and Analysis
6 Conclusion and Future Work
References
Logics for Program or System Verification
Behavioral Program Logic
1 Introduction
2 Preliminaries: An Actor Language with Futures
3 Behavioral Program Logic
4 A Sequent Calculus for BPL: Behavioral Types
5 Conclusion and Related Work
References
Prenex Separation Logic with One Selector Field
1 Introduction
2 Preliminaries
2.1 First Order Logic
2.2 Separation Logic
2.3 Test Formulas for SLk
3 From Infinite to Finite Satisfiability
4 PRE(SL1) is Decidable but Not Elementary Recursive
5 The BSR(SL1) Fragment is PSPACE-complete
6 Conclusion
References
Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems
1 Introduction
2 Technical Approach
3 Syntax of d4L
3.1 d4L Terms and Formulas
3.2 Doxastic Hybrid Programs
4 Semantics of d4L
5 Sound Sequent Calculus
6 Validation and Application
7 Related Work
8 Conclusions
References
Operational Semantics and Program Verification Using Many-Sorted Hybrid Modal Logic
1 Introduction
2 Preliminaries: A Many-Sorted Polyadic Modal Logic
3 Many-Sorted Hybrid Modal Logic
4 A SMC-like Language and a Hoare-Like Logic for It
5 Conclusions and Related Work
A Proofs from Sect.3
B Proofs from Sect.4
References
Author Index

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Automated Reasoning with Analytic Tableaux and Related Methods

Description

More details

Other editions

Additional editions

Content

System requirements