View: session overviewtalk overview

11:00 | ABSTRACT. Our main result is a doubly exponential decision procedure for the first-order equality theory of streams with both arithmetic and control-oriented stream operations. This stream logic is shown to be expressive for solving basic problems of stream calculus. |

11:30 | What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? PRESENTER: Quentin Petitjean ABSTRACT. The predicate definitions in Separation Logic (SL) play an important role: they introduce disjunctions and existential quantifications in fragments of SL not allowing the complete boolean fragment, and they capture a large spectrum of unbounded heap shapes due to their inductiveness. This expressiveness power comes with a limitation: the entailment problem is undecidable if predicates have general inductive definitions (ID). Iosif et al. proposed syntactic and semantic conditions, called PCE, on the ID of predicates to ensure the decidability of the entailment problem. We provide a (possibly non terminating) algorithm to transform arbitrary ID into equivalent PCE definitions, when possible. We show that the existence of an equivalent PCE definition for a given ID is undecidable, but we identify necessary conditions that are decidable. |

12:00 | Uniform Substitution for Differential Refinement Logic ABSTRACT. This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneously reason about properties of and relations between hybrid systems. Uniform substitution is the key to parsimonious prover kernels. It enables the verbatim use of axioms instead of axiom schemata with soundness-critical side conditions scattered across the proof calculus. The uniform substitution rule can then be used to instantiate all axioms soundly. Access to differential variables enables more control over the notion of refinement, which is shown to be decidable on a fragment of hybrid programs. |

14:00 | Sequents vs hypersequents for Aqvist systems ABSTRACT. Enhancing cut-free expressiveness through minimal structural additions to sequent calculus is a natural step. We focus on Aqvist's system F with cautious monotonicity (CM), a deontic logic extension of S5, for which we define a sequent calculus employing (semi) analytic cuts. The transition to hypersequents is key to develop modular and cut-free calculi for F+(cm) and G, also supporting countermodel construction. |

14:30 | Sequent Systems on Undirected Graphs ABSTRACT. In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce logical connectives allowing us to extend the well-known correspondence between classical propositional formulas and cographs. We define sequent systems operating on formulas containing such connectives, and we prove, using an analyticity argument based on cut-elimination, that our systems provide conservative extensions of multiplicative linear logic (without and with mix) and classical propositional logic. We conclude by showing that one of our systems captures graph isomorphism as logical equivalence, and that it is sound and complete for the graphical logic \GS. |

15:00 | A proof theory of (omega) context-free languages, via non-wellfounded proofs PRESENTER: Abhishek De ABSTRACT. We investigate the proof theory of regular expressions with fixed points, construed as a notation for context-free (omega-)grammars. Starting with a hypersequential system for regular expressions due to Das and Pous, we define its extension by least fixed points, and prove soundness and completeness of its non-wellfounded proofs for the standard language model. From here we apply proof theoretic techniques to recover an infinitary axiomatisation of the resulting equational theory, complete for inclusions of context-free languages. Finally we extend our syntax by greatest fixed points, now computing context-free omega-languages. We show soundness and completeness of the corresponding system using a mixture of proof theoretic and game theoretic techniques. |

15:30 | A cyclic proof system for Guarded Kleene Algebra with Tests ABSTRACT. Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT makes ordinary sequents sufficient for achieving regular completeness, unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the proof search induces a coNP decision procedure, rather than one in PSPACE. |

14:00 | An Empirical Assessment of Progress in Automated Theorem Proving ABSTRACT. The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. This work uses data in the TPTP World to assess progress in ATP from 2015 to 2023. |

14:30 | Reducibility Constraints in Superposition ABSTRACT. Modern superposition inference systems aim at reducing the search space by introducing redundancy criteria on clauses and inferences. This paper focuses on reducing the number of superposition inferences with a single clause by blocking inferences into some terms, provided there were previously made inferences of a certain form performed with predecessors of this clause. Other calculi based on blocking inferences, for example basic superposition, rely on variable abstraction or equality constraints to express irreducibility of terms, resulting however in blocking inferences with all subterms of the respective terms. Here we introduce reducibility constraints in superposition to enable a more expressive blocking mechanism for inferences. We show that our calculus remains (refutationally) complete and present redundancy notions. Our implementation in the Vampire prover demonstrates a great reduction in the size of the search space when using our new calculus. |

15:00 | First-Order Automatic Literal Model Generation ABSTRACT. Given a finite consistent set of ground literals, we present an algorithm that generates a complete first-order logic interpretation, i.e., an interpretation for all ground literals over the signature and not just those in the input set, that is also a model for the input set. The interpretation is represented by first-order linear literals. It can be effectively used to evaluate clauses. A particular application are SCL stuck states. The SCL calculus always computes with respect to a finite number of ground literals. It then finds either a contradiction or a stuck state being a model with respect to the considered ground literals. Our algorithm builds a complete literal interpretation out of such a stuck state model that can then be used to evaluate the clause set. If all clauses are satisfied an overall model has been found. If it does not satisfy some clause, this information can be effectively explored to extend the scope of ground literals considered by SCL. |

15:30 | Regularization in Spider-style Strategy Discovery and Schedule Construction PRESENTER: Filip Bártek ABSTRACT. To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In the Vampire prover, schedules were for a long time constructed by Andrei Voronkov using a tool called Spider, about which little was officially known until recently. After Andrei Voronkov's talk at the Vampire Workshop 2023, we decided to analyse this powerful technology on our own. In this paper, we report on a large-scale experiment with discovering Vampire strategies targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, but also estimate how well can a schedule be expected to generalize to unseen problems and what factors influence this property. |