Abstract Commonly used proof strategies by automated reasoners organise proof search either by ordering-based saturation or by reducing goals to subgoals. In this paper, we combine these two approaches and advocate a SAT-based method with symmetry breaking for connection calculi in first-order logic, with the purpose of further pushing the automation in first-order classical logic proofs. In contrast to classical ways of reducing first-order logic to propositional logic, our method encodes the structure of the proof search itself. We present three distinct SAT encodings for connection calculi, analyse their theoretical properties, and discuss the effect of using SAT/SMT solvers on these encodings. We implemented our work in the new solver UPCoP and showcase its practical feasibility.

Abstract We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition. Using these methods allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.

Abstract Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the classical first-order connection calculus, while retaining completeness. An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice. The approach may be useful for proof search in other non-confluent tableau calculi.

We introduce modular calculi for the logics for nonmonotonic reasoning defined by Kraus, Lehmann, and Magidor, featuring a strengthened form of analyticity. Our calculi are used to determine the computational complexity for the logics C, CL, CM, P (and M), and fragments thereof. The calculi are encoded into SMT solvers, yielding an efficient prover with countermodel generation capabilities. Our work encompasses known results and introduces new findings, including co-NP-completeness and a more effective semantics for C.

Abstract We show that tableau methods for satisfiability in non-classical logics can be supported naturally in SMT solving via the framework of user-propagators. By way of demonstration, we implement the description logic $$\mathcal {ALC}$$ in the Z3 SMT solver and show that working with user-propagators allows us to significantly outperform encodings to first-order logic with relatively little effort. We promote user-propagators for creating solvers for non-classical logics based on tableau calculi.