Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings

Preface
Organization
Abstracts of Invited Talks
The Strange Career of Interpolation and Definability
Rational Synthesis
The Barter Trade in Structure and Cuts
Comparing Rules for Identity in Sequent Systems and Natural Deduction
Forgetting and Subontology Generation for the Medical Ontology SNOMED CT
Contents
Tableau Calculi
Tableaux and Restricted Quantification for Systems Related to Weak Kleene Logic
	1 Introduction
	2 Weak Kleene Logic
		2.1 The Propositional Case
		2.2 Adding Restricted Quantifiers
		2.3 Brief Excursus on Quantification
		2.4 Tableau Calculus for Weak Kleene Logic with Restricted Quantifiers
	3 Bilateral Logics Related to Weak Kleene Logic
		3.1 Sfde and AC
		3.2 Adding Restricted Quantifiers
		3.3 Tableau Calculi for Sfde and AC with Restricted Quantifiers
	4 Concluding Remarks
	References
Constraint Tableaux for Two-Dimensional Fuzzy Logics
	1 Introduction
	2 The Logics for a Two-Dimensional Treatment of Uncertainty
		2.1 Preliminaries
		2.2 The Logics
		2.3 Semantical Properties of ŁŁŁŁ2(x,y)()
		2.4 Semantical Properties of G2()
	3 Tableaux
		3.1 Constraint Tableaux for ŁŁŁŁ2
		3.2 Constraint Tableaux for G2
		3.3 Applications
	4 Conclusions and Further Research
	References
Analytic Tableaux for Non-deterministic Semantics
	1 Introduction
	2 Non-deterministic Semantics
	3 Tableau System Definition
	4 Rule Construction
	5 Soundness
	6 Completeness
	7 DNF Representations
		7.1 Canonical DNF
	8 Related Work
		8.1 Analytic Tableaux for Many-Valued Logic
		8.2 Dual Tableaux
		8.3 Canonical Calculi
		8.4 Other Calculi
		8.5 Semantic Games
	9 Conclusion
	References
Tableaux for Free Logics with Descriptions
	1 Introduction
	2 Preliminaries
		2.1 Syntax
		2.2 Semantics
	3 Tableau Calculi
	4 Soundness and CompletenessFull Versions of the Proofs of Lemmas 3 and 4 and Propositions 1 and 2 Can Be Found in ch4IndZaw21.
		4.1 Soundness
		4.2 Completeness
	5 Related Work
	6 Conclusions
	References
CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-Learning and SAT
	1 Introduction
	2 Modal Clausal Tableaux
	3 SAT-solvers and the CEGAR Procedure
		3.1 Counter-Example Guided Abstraction Refinement (CEGAR)
	4 CEGAR Tableaux: Modal Clause-Learning via SAT
		4.1 Termination, Soundness and Completeness of the Strategy
	5 Implementation: Our Modal Satisfiability Tester CEGARBox
		5.1 Initialising a Trie During Normal Forming
		5.2 The Main Algorithm
		5.3 Inputs and Outputs
		5.4 Use of Satisfiability Under Unit Assumptions
		5.5 Modal Clause Learning Modifies the Modal Context at Level i
	6 Extensions to KT and S4
	7 Optimisations Which Made CEGARBox faster
		7.1 Reducing the Number of Dia-Clauses
		7.2 Memoisation of Satisfiable Assumptions
		7.3 Two Phase Caching
	8 Benchmarks and Issues with MOSAIC
	9 Experimental Results
	10 Related Work
	11 Further Work and Conclusions
	References
Sequent Calculi
Proof-Theory and Semantics for a Theory of Definite Descriptions
	1 Introduction
	2 A Deductive Calculus for Classical Positive Free Logic with a Binary Quantifier
	3 Consequences of the Formalisation
	4 Cut Elimination for CPFI
	5 Semantics for CPFI
	6 Soundness and Completeness
	7 Tableaux Rules
	8 Conclusion
	References
Basing Sequent Systems on Exclusive-Or
	1 Introduction
	2 Preliminaries
	3 The Basic Systems
	4 Theorems on Strong Completeness
	5 Enhancing the Expressive Power of the System
	References
Proof Search on Bilateralist Judgments over Non-deterministic Semantics
	1 Introduction
	2 Preliminaries
		2.1 Languages
		2.2 Two-Dimensional Consequence Relations
		2.3 Two-Dimensional Non-deterministic Matrices
		2.4 Calculi for Two-Dimensional Statements
	3 Axiomatizing Monadic []-matrices
	4 Proof Search in Two Dimensions
	5 Conclusion
	References
From Input/Output Logics to Conditional Logics via Sequents – with Provers
	1 Introduction
	2 Input/Output Logics and Their Sequent Calculi
	3 Technical Results and Correspondence
	4 Theorem Proving
	5 Conclusion
	References
Theorem Proving
Towards Finding Longer Proofs
	1 Introduction
	2 Related Work
	3 The leanCoP Connection Tableau Calculus
	4 FLoP – Main Algorithm
		4.1 Reinforcement Learning Fundamentals
		4.2 Reinforcement Learning in FLoP
		4.3 Curriculum Learning
		4.4 Training Algorithm
		4.5 Implementation Details
	5 Datasets
	6 Experiments
	7 Conclusion and Future Work
	References
lazyCoP: Lazy Paramodulation Meets Neurally Guided Search
	1 Introduction
	2 Related Work
	3 Unguided System
		3.1 Connection Tableaux
		3.2 Lazy Paramodulation
		3.3 Calculus Refinements
	4 Proof Search
		4.1 Policy-Guided Search
		4.2 Asynchronous Policy Evaluation
	5 Learned Policy
		5.1 Representing Tableaux with Actions
		5.2 Network Architecture
		5.3 Training
		5.4 Integration and Optimisation
	6 Experimental Results
		6.1 Inference Rates
		6.2 Effect of Guidance
	7 Conclusion and Future Work
	References
AC Simplifications and Closure Redundancies in the Superposition Calculus
	1 Introduction
	2 Preliminaries
	3 Model Construction
	4 Redundancies
	5 Experimental Results
	6 Conclusion and Future Work
	References
The Role of Entropy in Guiding a Connection Prover
	1 Introduction
	2 Background and Related Work
		2.1 Neural Feature Extraction for Guiding Theorem Provers
		2.2 Systems Guiding the leanCoP Theorem Prover
		2.3 Reinforcement Learning (RL)
		2.4 Monte Carlo Tree Search (MCTS)
		2.5 Maximum Entropy Reinforcement Learning
		2.6 Kullback-Leibler Divergence
	3 Maximum Entropy for MCTS and Theorem Proving
		3.1 Exploration and Entropy in MCTS
		3.2 Normalized Entropy
		3.3 Temperature-Based and Regularization-Based Entropy Control
	4 Entropy Regularized Neural Guidance for plCoP
		4.1 Neural Representation of the State and Inference Steps
		4.2 Training the Policy and Value Guidance for MCTS
	5 Experiments
		5.1 Datasets and Common Settings
		5.2 Experiment 1: Influence of Entropy Regularization
		5.3 Experiment 2: Relative Entropy on the Same Proof States
		5.4 Experiment 3: Order and Entropy Are Largely Sufficient
		5.5 Experiment 4: Temperature vs. Entropy Regularization
		5.6 Experiment 5: Final Large Train/Test Evaluation on Mizar40
	6 Conclusion
	References
The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics
	1 Introduction
	2 Non-clausal Connection Calculi
	3 The Implementations
		3.1 Non-clausal Matrix
		3.2 nanoCoP for Classial Logic
		3.3 nanoCoP-i for Intuitionistic Logic
		3.4 nanoCoP-M for Multimodal Logics
		3.5 Proof Search Optimizations
		3.6 Proof Output
	4 Experimental Evaluation
	5 Conclusion
	References
Eliminating Models During Model Elimination
	1 Introduction
	2 Preliminaries
		2.1 Connection Tableau Systems
		2.2 Boolean Satisfiability
		2.3 Ground Support for First-Order Reasoning
		2.4 First-Order Benchmarks
	3 Research Vehicle: SATCoP
	4 Grounding Clausal Tableaux
		4.1 Reporting Unsatisfiability
		4.2 Grounding Schemes
		4.3 SAT Solving
		4.4 A Note on Proofs
	5 Randomisation and Depth Control
	6 Model-Based Lemmata
	7 First Impressions
	8 Experimental Evaluation
		8.1 System Configurations
		8.2 Results and Discussion
	9 Conclusions and Future Directions
		9.1 A Note from the Future
	References
Learning Theorem Proving Components
	1 Introduction: Clause Selection and Context
	2 ENIGMA and Learning Context-Based Guidance
	3 Leapfrogging
	4 Learning Reasoning Components
	5 Clustering Methods
		5.1 Clustering
	6 Evaluation
		6.1 Leapfrogging
		6.2 Splitting and Merging
	7 Conclusion
	References
Formalized Proofs
A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic
	1 Introduction
	2 Preliminaries
		2.1 A Linear Nested Sequent Calculus for Kt
	3 Encoding Formulae, Sequents and LNSs
	4 Encoding the LNSKt Calculus
	5 Encoding Derivability
	6 Proof Theoretic Properties of LNSKt
	7 Cut-Elimination via Cut-Admissibility
		7.1 Cut-Admissibility
		7.2 The Main Lemma: ``Lemma Sixteen\'\'
		7.3 Cut-Elimination
	8 Extraction
	9 Related Work
	10 Conclusion and Future Work
	References
Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq
	1 Introduction
	2 Various Issues with the Method Used by Brighton
	3 Preliminaries
	4 Properties Of GLS
	5 PSGLS: A Terminating Proof-Search
	6 Cut-Elimination for GLS
	7 Conclusion
	References
Non-Wellfounded Proofs
Complexity of a Fragment of Infinitary Action Logic with Exponential via Non-well-founded Proofs
	1 Introduction
	2 Formulation of !ACT
	3 Non-well-founded Proofs
	4 Complexity
	5 Issues with *-Elimination
	6 Concluding Remarks
	References
Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus
	1 Introduction
	2 The Modal mu-calculus
	3 The JS proof system
	4 Uniform Interpolation
	5 Constructing the Interpolant
	6 Verifying the Interpolant
	7 Conclusion
	References
Cyclic Hypersequent Calculi for Some Modal Logics with the Master Modality
	1 Introduction
	2 Preliminaries
	3 Infinitary and Cyclic Hypersequent Calculi
		3.1 Hypersequents and Pre-proofs
		3.2 Infinitary Proofs with Trace Condition
		3.3 Cyclic Proofs
	4 Soundness
	5 Completeness
		5.1 Completeness of HK*circ + RC for Equable C
		5.2 Completeness via (Infinitary) Proof Search
	6 Conclusion
	References
A Focus System for the Alternation-Free -Calculus
	1 Preliminaries
	2 The Focus System
		2.1 The Proof Systems Focus and Focus
		2.2 Circular and Infinite Proofs
		2.3 Thin and Progressive Proofs
	3 Tableaux and Tableau Games
	4 Soundness
	5 Completeness
	6 Conclusion and Questions
	References
Intuitionistic Modal Logics
Terminating Calculi and Countermodels for Constructive Modal Logics
	1 Introduction
	2 Constructive Modal Logics and Their Semantics
	3 Sequent Calculi
	4 Refutation Calculi and Countermodel Construction
	5 Conclusion and Future Work
	References
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
	1 Introduction
	2 Logical Preliminaries
	3 Grammar Theoretic Preliminaries
	4 Labelled Sequent Systems
	5 Structural Refinement
	6 Nested Sequent Systems
	7 Conclusion
	References
Game Semantics for Constructive Modal Logic
	1 Introduction
	2 Background
		2.1 Constructive Modal Logic
		2.2 Modal Arenas
	3 Winning Strategies for CK
	4 Compositionality of Winning Strategies
	5 Game Semantics for Constructive Modal Logic
		5.1 Game Semantics for CD
	6 Conclusion and Future Work
	References
The Došen Square Under Construction: A Tale of Four Modalities
	1 Introduction
		1.1 State of the Art
		1.2 Contributions
	2 The Došen Square CKD of Constructive Modalities
	3 Proof Systems for CKD
		3.1 CKD Global Reasoning: The Hilbert Calculus HCKD
		3.2 Landing at Došen Square: The Sequent Calculus GCKD
	4 Conclusion
	References
Author Index