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(Herausgeber*in)

Springer (Verlag)

Erschienen am 22. August 2019

XXI, 477 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

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

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken