ABSTRACT. Satisfiability checking is a research area devoted to the development and implementation of algorithms for the automated satisfiability check of logical formulas. SAT solving for propositional logic became impressively powerful due to an elegant combination of a smart search space exploration and proof construction. This idea has been later generalized to quantifier-free first-order logic formulas over some theories, most notably quantifier-free real algebra, in the framework of the model constructing satisfiability calculus (MCSAT). Both approaches are based on the generalization of "wrong guesses" made by the exploration into pieces of a proof, which are collected and used to synthesize a global proof during the solving process. While being one of the currently best approaches, for large or complex formulas, a large number of "proof pieces" cause high effort for their processing and thus restrict scalability. Thus the question comes up whether there are ways to store such information in a more structured way, which requires lower costs for processing. This thought is taken up by the method of the cylindrical algebraic coverings, developed for the satisfiability check of conjunctions of polynomial constraints. In this talk, we will discuss the above ideas and methods, and highlight their relations and differences.

ABSTRACT. We introduce Virtual Integer-Real Arithmetic Substitution (VIRAS), a quantifier elimination procedure for deciding quantified linear mixed integer-real arithmetic problems. VIRAS combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that VIRAS gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve.

ABSTRACT. This is part of an ongoing research project, with the aim of studying the connections between model-theoretic properties related to theory combination in Satisfiability Modulo Theories. In previous work, 7 properties were analyzed: convexity, stable infiniteness, smoothness, finite witnessibility, strong finite witnessibility, the finite model property, and stable finiteness.

The first two properties are needed for Nelson-Oppen combination, the third and fourth are related to polite combination, the third and fifth correspond to strong politeness, and the last two are related to the combination of shiny theories.

However, the remaining key property of shiny theories, namely, the ability to compute the cardinalities of minimal models, was not yet analyzed. In this paper we study this property.

ABSTRACT. Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order to extend the notion of context-free sets from words and trees to graphs of bounded tree-width. While for words and trees syntactic grammar restrictions are known that guarantee that the associated languages of words resp. trees are regular - and hence, MSO definable - the situation is more complicated for graphs. Here, Courcelle proposed the notion of regular graph grammars, a syntactic restriction of HR grammars that guarantees the definability of the associated languages of graphs in Counting Monadic Second Order Logic (CMSO). However, these grammars are not complete in the sense that not every CMSO definable set of graphs of bounded tree-width can be generated by a regular graph grammar. In this paper, we introduce a new syntactic restriction of HR grammars, called tree-verifiable graph grammars, and a new notion of bounded tree-width, called embeddable bounded tree-width, where the later restricts the trees of a tree-decomposition to be a subgraph of the analyzed graph. The main property of tree-verifiable graph grammars is that their associated languages are CMSO definable and that the have bounded embeddable tree-width. We show further that they strictly generalize the regular graph grammars of Courcelle. Finally, we establish a completeness result, showing that every language of graphs that is CMSO definable and of bounded embeddable tree-width can be generated by a tree-verifiable graph grammar.

ABSTRACT. One of the main challenges in the area of Neuro-symbolic AI is to perform logical reasoning in the presence of neural and symbolic datasets. This requires the combination of heterogeneous data sources such as knowledge graphs, neural model predictions, structured databases, crowd-sourced data, and many more. In this paper we introduce $t$-Datalog$^\exists$ as a formalism for such reasoning tasks, $t$-Datalog$^\exists$ generalises of Datalog with existential rules or Datalog$^\exists$ (also commonly referred to as tuple-generating dependencies) by allowing the use of arbitrary t-norms in place of classical conjunction in rule bodies. The resulting formalism combines the best of both worlds. It extends the power and flexibility of Datalog$^\exists$ to neuro-symbolic reasoning tasks while preserving many of the desirable properties of the classical case. In particular, we show that natural extensions of the chase to our setting produces \emph{fuzzy universal models}, and that the complexity of reasoning in important decidable fragments remains the same as in the classical setting.

ABSTRACT. Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together without making use of an encoding into a common target framework. This work proposes an intersection type system for PCF with a specific notion of evaluation, called PCFH. Although this form of evaluation is sometimes referred to as “call-by-value”, evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV-like operational behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only that typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the normalization sequences to normal form. This type system is then refined to a tight one, offering exact information regarding the length of normalization sequences.

ABSTRACT. We provide the first proof of confluence for cut elimination in multiplicative-exponential linear logic proof-nets that is not based on Newman's lemma or strong normalization, not even indirectly. To achieve our goal, we take inspiration from Tait and Martin-Lof's method based on parallel reduction for the lambda-calculus, even though the wilder realm of untyped proof-nets makes the proof subtler and more challenging.

ABSTRACT. Deep inference is a proof theoretical formalism that generalises the “shallow inference” of the sequent calculus by permitting the application of inference rules like term rewriting rules. Deep inference makes it possible to access shorter proofs than sequent calculus; however, with the cost of increased nondeterminism, an obstacle in front of proof search applications. Deep inference is essential for designing system BV, an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. MLL has shallow inference systems, whereas BV is impossible with a shallow-only system. As Tiu showed, any restriction on rule depth makes a system incomplete for BV. This paper shows that any restriction that rules out shallow rules makes the system incomplete, too. Our results indicate that for system BV, shallow and deep rules must coexist for completeness. We provide extensive empirical evidence that deep inference can still be faster than shallow inference when used strategically with a proof theoretical technique for reducing nondeterminism. We show that prioritising deeper rule instances reduces the cost of proof search by reducing the size of the managed contexts, consequently providing more immediate access to shorter proofs. Moreover, we identify a class of MLL formulae with deep inference proof search times that grow linearly in the number of atoms in contrast to an exponential growth pattern with shallow inference. We introduce a large and exhaustive benchmark for MLL, with and without mix, and a proof search framework to apply various search strategies, which should be of independent interest.

ABSTRACT. TBA

ABSTRACT. TBA

ABSTRACT. TBA

ABSTRACT. TBA