ABSTRACT. The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem that lies at the core of many questions in this setting is the following: given a set of pairs of rational weights and matrices {(w1, A1), . . . , (wm, Am)}, we ask if the weighted sum of powers of these matrices is eventually non-negative (resp. positive), i.e., does there exist an integer N s.t for all n greater than N , (w1.A1^n + w2.A2^n+ ... + w_m.Am^n) \geq 0 (resp. > 0). The restricted setting when m = w1 = 1, results in so-called eventually non-negative (or eventually positive) matrices, which enjoy nice spectral properties and have been well-studied in control theory. More applications arise in varied contexts, ranging from program verification to partially observable and multi-modal systems.

Our goal is to investigate this problem and its link to linear recurrence sequences. Our first result is that for m > 1, the problem is as hard as the ultimate positivity of linear recurrences, a long standing open question (known to be coNP-hard). Our second result is a reduction in the other direction showing that for any m \geq 1, the problem reduces to ultimate positivity of linear recurrences. This shows precise upper bounds for several subclasses of matrices by exploiting known results on linear recurrence sequences. Our third main result is an effective algorithm for the class of diagonalizable matrices, which goes beyond what is known on linear recurrence sequences.

ABSTRACT. Explanations for description logic (DL) entailments provide important support for the design and maintenance of large ontologies. The "justifications" usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which not only visualizes proofs of consequences for ontologies written in expressive DLs, but also offers several proof generation procedures and various functions for condensing large proofs.

ABSTRACT. Proof production for SMT solvers is paramount to ensure their correctness independently from implementations, which are often prohibitively complex to be verified. However, historically SMT proof production has struggled with performance and coverage issues, with many crucial solving techniques being disabled, and lack of details, with hard to check, coarse-grained proofs. Here we present a flexible proof production architecture designed to handle the complexity of versatile, industrial-strength SMT solvers, and how we leveraged it to produce detailed proofs, including for previously unsupported components by any solver. The architecture allows proofs to be produced modularly, lazily and with numerous safeguards for correct generation. This architecture has been implemented in the state-of-the-art SMT solver cvc5. We evaluate its proofs for SMT-LIB benchmarks and show the new architecture allows better coverage than previous approaches, has acceptable performance overhead, and allows detailed proofs for most solving components.

ABSTRACT. Choice logics constitute a family of propositional logics and are used for the representation of preferences, with especially qualitative choice logic (QCL) being an established formalism with numerous applications in artificial intelligence. While computational properties and applications of choice logics have been studied in the literature, only few results are known about the proof-theoretic aspects of their use. We propose a sound and complete sequent calculus for preferred model entailment in QCL, where a formula F is entailed by a QCL-theory T if F is true in all preferred models of T. The calculus is based on labeled sequent and refutation calculi, and can be easily adapted for different purposes. For instance, using the calculus as a cornerstone, calculi for other choice logics such as conjunctive choice logic (CCL) can be obtained in a straightforward way.

ABSTRACT. We introduce a~paraconsistent modal logic $\KGsquare$, based on Gödel logic with coimplication (bi-Gödel logic) expanded with a De Morgan negation $\neg$. We use the logic to formalise reasoning with graded, incomplete and inconsistent information. Semantics of $\KGsquare$ is two-dimensional: we interpret $\KGsquare$ on crisp frames with two valuations $v_1$ and $v_2$, connected via $\neg$, that assign to each formula two values from the real-valued interval $[0,1]$. The first (resp., second) valuation encodes the positive (resp., negative) information the state gives to a~statement. We obtain that $\KGsquare$ is strictly more expressive than the classical modal logic $\mathbf{K}$ by proving that finitely branching frames are definable and by establishing a faithful embedding of $\mathbf{K}$ into $\KGsquare$. We also construct a~constraint tableau calculus for $\KGsquare$ over finitely branching frames, establish its decidability and provide a~complexity evaluation.

ABSTRACT. Adding multi-modalities (called subexponentials) to linear logic enhances its power as a logical framework, which has been extensively used in the specification of e.g. proof systems, programming languages and bigraphs. Initially, subexponentials allowed for classical, linear, affine or relevant behaviors. Recently, this framework was enhanced so to allow for commutativity as well. In this work, we close the cycle by considering associativity. We show that the resulting system (acLL) admits the (multi)cut rule, and we prove two undecidability results for fragments/variations of acLL.

ABSTRACT. We consider a logic used to describe sets of configurations of distributed systems, whose network topologies can be changed at runtime, by reconfiguration programs. The logic uses inductive definitions to describe networks with an unbounded number of components and interactions, written using a multiplicative conjunction, reminiscent of Bunched Implications and Separation Logic. We study the complexity of the satisfiability and entailment problems for the configuration logic under consideration. Additionally, we consider degree boundedness (is every component involved in a bounded number of interactions?), an ingredient for decidability of entailments.

ABSTRACT. The importance of subsumption testing for redundancy elimination in first-order logic automatic reasoning is well-known. Although the problem is already NP-complete for first-order clauses, the meanwhile developed test pipelines efficiently decide subsumption in almost all practical cases. We consider subsumption between first-oder clauses of the Bernays-Schönfinkel fragment over linear, real arithmetic constraints: BS(LRA). The bottleneck in this setup is deciding implication between the LRA constraints of two clauses. Our new sample point heuristic preempts expensive implication decisions in about 94% of all cases in benchmarks. Combined with filtering techniques for the first-order BS part of clauses, it results again in an efficient subsumption test pipeline for BS(LRA) clauses.

ABSTRACT. Lash is a higher-order automated theorem prover created as a fork of the theorem prover Satallax. The basic underlying calculus of Satallax is a ground tableau calculus whose rules only use shallow information about the terms and formulas taking part in the rule. Lash uses new, efficient C representations of vital structures and operations. Most importantly, Lash uses a C representation of (normal) terms with perfect sharing along with a C implementation of normalizing substitutions. We describe the ways in which Lash differs from Satallax and the performance improvement of Lash over Satallax when used with analogous flag settings. With a 10s timeout Lash outperforms Satallax on a collection TH0 problems from the TPTP. We conclude with ideas for continuing the development of Lash.

ABSTRACT. We describe Goéland, an automated theorem prover for first-order logic that relies on a concurrent search procedure to find tableau proofs, with concurrent processes corresponding to individual branches of the tableau. Since branch closure may require instantiating free variables shared across branches, processes communicate via channels to exchange information about substitutions used for closure. We present the proof-search procedure and its implementation, as well as experimental results obtained on problems from the TPTP library.

ABSTRACT. We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded as description logic knowledge bases. We introduce an action language to model mutating actions; that is, actions that change the structural configuration of a given deployment by adding, modifying, or deleting resources. We mainly focus on two problems: the problem of determining whether the execution of an action, no matter the parameters passed to it, will not cause the violation of some security requirement (static verification), and the problem of finding sequences of actions that would lead the deployment to a state where (un)desirable properties are (not) satisfied (plan existence and plan synthesis). For all these problems, we provide definitions, complexity results, and decision procedures.

ABSTRACT. We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic (PDL), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and PDL, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, requiring alternating automata for proof checking and necessitating a more intricate soundness argument than for traditional cyclic proofs.

ABSTRACT. Theories axiomatised by unit equalities include problems in group theory, loops, lattices, and other algebraic structures are notoriously difficult for general purpose theorem provers. Provers specialised for unit equational theories (UEQ) are based on Knuth-Bendix (KB) completion in contrast to provers applicable to general equational problems which are based on the superposition calculus. Although Knuth-Bendix completion and superposition are closely related, a number of simplifications which make Knuth-Bendix completion efficient are not available in superposition.

In particular, key simplifications such as ground joinability, although known for more than 30 years, have not been extended from KB completion to superposition. In fact, all previous completeness proofs for ground joinability rely on proof orderings and proof reductions, which are not easily extensible to general clauses together with redundancy elimination. In this paper we address this limitation and extend superposition with ground joinability, and show that under an adapted notion of redundancy, simplifications based on ground joinability preserve completeness.

Another recently introduced simplification for UEQ is connectedness. We extend this notion to “ground connectedness” and show superposition is complete with both connectedness and ground connectedness.

We implemented ground joinability in a theorem prover, iProver, using a novel algorithm which we also present in this paper, and evaluated over the TPTP library with encouraging results.

ABSTRACT. Equational unification and matching are fundamental mechanisms in many automated deduction applications. Supporting them efficiently for as wide as possible a class of equational theories, and in a typed manner supporting type hierarchies, benefits many applications; but this is both challenging and nontrivial. We present Maude 3.2’s efficient support of these features as well as of symbolic reachability analysis of infinite-state concurrent systems based on them.

ABSTRACT. The analysis of complex dynamic systems is a core research topic in formal methods and AI, and combined modelling of systems with data has gained increasing importance in applications such as business process management. In addition, process mining techniques are nowadays used to automatically mine process models from event data, often without correctness guarantees. Thus verification techniques for linear and branching time properties are needed to ensure desired behavior. Here we consider data-aware dynamic systems with arithmetic (DDSAs), which constitute a concise but expressive formalism of transition systems with linear arithmetic guards. We present a CTL* model checking procedure for DDSAs that relies on a finite-state abstraction by means of a set of formulas that capture variable configurations. Linear-time verification was shown to be decidable in specific classes of DDSAs where the constraint language or the control flow are suitably confined. We investigate several of these restrictions for the case of CTL*, with both positive and negative results: CTL* verification is proven decidable for monotonicity and integer periodicity constraint systems, but undecidable for feedback free and bounded lookback systems. To witness the feasibility of our approach, we implemented it in the SMT-based prototype ada. It turns out that many practical business process models can be effectively analyzed by our tool.

ABSTRACT. We present a decision procedure for intermediate logics relying on a modular extension of the SAT-based proof search-engine intuitR for intuitionistic propositional logic. Given the module for the intermediate logic L, our procedure iteratively searches for a Kripke countermodel for a formula A, exploiting the search engine of intuitR: whenever a countermodel for A is built, the module checks whether it is a model of the logic L. If this is the case A is not valid in L. Otherwise, the module provides an instance of an axiom of L falsified in the countermodel that is fed to the SAT-solver for a new try. We prove the partial correctness of our procedure and its termination for some well-known intermediate logics.

ABSTRACT. We present the Loop Acceleration Tool (LoAT), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on a novel calculus for loop acceleration, i.e., transforming loops into non-deterministic straight-line code, and for finding non-terminating configurations. To implement it efficiently, LoAT uses a new approach based on unsat cores. We evaluate LoAT's power and performance by extensive experiments.

ABSTRACT. Definition packages in theorem provers provide users with means of defining and organizing concepts of interest. This system description presents a new definition package for the hybrid systems theorem prover KeYmaera X based on differential dynamic logic (dL). The package adds KeYmaera X support for user-defined smooth functions whose graphs can be implicitly characterized by dL formulas. Notably, this makes it possible to implicitly characterize functions, such as the exponential and trigonometric functions, as solutions of differential equations and then prove properties of those functions using dL's differential equation reasoning principles. Trustworthiness of the package is achieved by minimally extending KeYmaera X's soundness-critical kernel with a single axiom scheme that expands function occurrences with their implicit characterization. Users are provided with a high-level interface for defining functions and non-soundness-critical tactics that automate low-level reasoning over implicit characterizations in hybrid system proofs.

ABSTRACT. Abduction is the task of finding possible extensions of a given knowledge base that would make a given sentence logically entailed. As such, it can be used to explain why the sentence does not follow, to repair incomplete knowledge bases, and to provide possible explanations for unexpected observations. We consider TBox abduction in the lightweight description logic EL, where the observation is a concept inclusion and the background knowledge is a description logic TBox. To avoid useless answers, such problems usually come with further restrictions on the solution space and/or minimality criteria that help sort the chaff from the grain. We argue that existing minimality notions are insufficient, and introduce connection minimality. This criterion rejects hypotheses that use concept inclusions “disconnected” from the problem at hand. We show how to compute a special class of connection-minimal hypotheses in a sound and complete way. Our technique is based on a translation to first-order logic, and constructs hypotheses based on prime implicates. We evaluate a prototype implementation of our approach on ontologies from the medical domain.

ABSTRACT. A clause $C$ is syntactically relevant in some clause set $N$, if it occurs in every refutation of $N$. A clause $C$ is syntactically semi-relevant, if it occurs in some refutation of $N$. While syntactic relevance coincides with satisfiability, i.e., if $C$ is syntactically relevant $N\setminus\{C\}$ is satisfiable, the semantic counterpart for syntactic semi-relevance was not known so far. Using the new notion of a \emph{conflict literal} we show that for independent clause sets $N$ a clause $C$ is syntactically semi-relevant in the clause set $N$ if and only if it adds to the number of conflict literals in $N$. A clause set is independent, if no clause out of the clause set is the consequence of different clauses from the clause set.

Furthermore, we relate the notion of relevance to that of a minimal unsatisfiable subset (MUS) of some independent clause set $N$. In propositional logic, a clause $C$ is relevant if it occurs in all MUSes of some clause set $N$ and semi-relevant if it occurs in some MUS. For first-order logic the characterization needs to be refined with respect to ground instances of $N$ and $C$.

ABSTRACT. A code $X$ is not primitivity preserving if there is a primitive list $\ws \in \lists X$ whose concatenation is imprimitive. We formalize a full characterization of such codes in the binary case in the proof assistant Isabelle/HOL. Part of the formalization, interesting on its own, is a description of $\{x,y\}$-interpretations of the square $xx$ if $\abs y \leq \abs x$. We also provide a formalized parametric solution of the related equation $x^jy^k = z^\ell$

ABSTRACT. The study of clause redundancy in Boolean satisfiability (SAT) has proven significant in various terms, from fundamental insights into preprocessing and inprocessing to the development of practical proof checkers and new types of strong proof systems. We study liftings of the recently-proposed notion of propagation redundancy---based on a semantic implication relationship between formulas---in the context of maximum satisfiability (MaxSAT), where of interest are reasoning techniques that preserve optimal cost (in contrast to preserving satisfiability in the realm of SAT). We establish that the strongest MaxSAT-lifting of propagation redundancy allows for changing in a controlled way the set of minimal correction sets in MaxSAT. This ability is key in succinctly expressing MaxSAT reasoning techniques and allows for obtaining correctness proofs in a uniform way for MaxSAT reasoning techniques very generally. Bridging theory to practice, we also provide a new MaxSAT preprocessor incorporating such extended techniques, and show through experiments its wide applicability in improving the performance of modern MaxSAT solvers.

ABSTRACT. The ontology of Le\'sniewski is commonly regarded as the most comprehensive calculus of names and the theoretical basis of mereology. However, ontology was not examined by means of proof-theoretic methods so far. In the paper we prowide a characterization of elementary ontology as a sequent calculus satisfying desiderata usually formulated for decent systems in modern structural proof theory. In particular, the cut elimination theorem is proved and the version of subformula property holds for the cut-free version.

ABSTRACT. The cvc5 SMT solver solves quantifier-free nonlinear real arithmetic problems by combining the cylindrical algebraic coverings method with incremental linearization in an abstraction-refinement loop. The result is a complete algebraic decision procedure that leverages efficient heuristics for refining candidate models. Furthermore, it can be used with quantifiers, integer variables, and in combination with other theories. We describe the overall framework, individual solving techniques, and a number of implementation details. We demonstrate its effectiveness with an evaluation on the SMT-LIB benchmarks.

ABSTRACT. Anti-unification aims at computing generalizations for given terms, retaining their common structure and abstracting differences by variables. We study quantitative anti-unification where the notion of the common structure is relaxed into "proximal" up to the given degree with respect to the given fuzzy proximity relation. Proximal symbols may have different names and arities. We develop a generic set of rules for computing minimal complete sets of approximate generalizations and study their properties. Depending on the characterizations of proximities between symbols and the desired forms of solutions, these rules give rise to different versions of concrete algorithms.

ABSTRACT. A four-valued semantics for the modal logic K is introduced. Possible worlds are replaced by a hierarchy of four-valued valuations, where the valuations of the first level correspond to valuations that are legal w.r.t. a basic non-deterministic matrix, and each level further restricts its set of valuations. The semantics is proven to be effective, and to precisely capture derivations in a sequent calculus for K of a certain form. Similar results are then obtained for the modal logic KT, by simply deleting one of the truth values.

ABSTRACT. We propose a new calculus SCL(EQ) for first-order logic with equality that only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption is used to guide inferences that are then guaranteed to be non-redundant. Redundancy is defined with respect to a dynamically changing ordering derived from the ground literal model assumption. We prove SCL(EQ) sound and complete and provide examples where our calculus improves on superposition.

ABSTRACT. There exist several results on deciding termination and computing runtime bounds for triangular weakly non-linear loops (twn-loops). We show how to use such results on subclasses of programs where complexity bounds are computable within incomplete approaches for complexity analysis of full integer programs. To this end, we present a novel modular approach which computes local runtime bounds for subprograms which can be transformed into twn-loops. These local runtime bounds are then lifted to global runtime bounds for the whole program. The power of our approach is shown by our implementation in the tool KoAT which analyzes complexity of programs where all other state-of-the-art tools fail.

ABSTRACT. A strategy schedule allocates time to different proof strategies in a theorem prover. We employ Bayesian statistics to propose a strategy schedule for each proof attempt. Tested on the TPTP problem library, our method yields a time saving of more than 50%. By extending this method to optimise the fixed time allocations to each strategy, we obtain a notable increase in the number of theorems proved.

ABSTRACT. We describe a system that detects an invariance in a problem expressed in a logical formula and simplifies it by eliminating variables utilizing the invariance. Pre-defined function and predicate symbols in the problem representation language are associated with algebraically indexed types, which signify the invariance property of them. A Hindley-Milner style type reconstruction algorithm is derived for detecting the invariance of a problem. In the experiment, the invariance-based formula simplification significantly enhanced the performance of a problem solver based on quantifier-elimination for real-closed fields, especially on the problems taken from the International Mathematical Olympiads.

ABSTRACT. The modal logic K is commonly used to represent and reason about necessity and possibility and its extensions with combinations of additional axioms is used to represent knowledge, belief, desires and intentions. Here we present local reductions of all propositional modal logics in the so-called modal cube, that is, extensions of K with arbitrary combinations of the axioms B, D, T, 4 and 5 to a normal form comprising a formula and the set of modal levels it occurs at. Using these reductions we can carry out reasoning for all these logics with the theorem prover KSP. We define benchmarks for these logics and experiment with the reduction approach as compared to an existing resolution calculus with specialised inference rules for the various logics.

ABSTRACT. Automated theorem provers (ATPs) are today used to attack open problems in several areas of mathematics. An ongoing project by Kinyon and Veroff uses Prover9 to search for the proof of the Abelian Inner Mapping (AIM) Conjecture, one of the top open conjectures in quasigroup theory. In this work, we improve Prover9 on a benchmark of AIM problems by neural synthesis of useful alternative formulations of the goal. In particular, we design the 3SIL (stratified shortest solution imitation learning) method. 3SIL trains a neural predictor through a reinforcement learning (RL) loop to propose correct rewrites of the conjecture that guide the search. 3SIL is first developed on a simpler, Robinson arithmetic rewriting task for which the reward structure is similar to theorem proving. There we show that 3SIL outperforms other RL methods. Next we train 3SIL on the AIM benchmark and show that the final trained network, deciding what actions to take within the equational rewriting environment, proves 70.2% of problems, outperforming Waldmeister (65.5%). When we combine the rewrites suggested by the network with Prover9, we prove 8.3% more theorems than Prover9 in the same time, bringing the performance of the combined system to 90%

ABSTRACT. I introduce substitutive sets, which are algebraic structures axiomatizing fundamental properties of variable-for-variable substitution on syntax with bindings. Substitutive sets compare favorably in some respects with the well-known foundation based on nominal sets. In particular, substitution is a more fundamental operator than the nominal swapping operator and enjoys a simpler, equationally expressed relationship with the variable-freshness predicate. Together with some natural axioms matching properties of the syntactic constructors, substitutive sets yield a truly minimalistic characterization of lambda-calculus terms as an abstract datatype, hence a recursion principle -- the first one in the literature that involves only unconditional equations on the constructors and substitution. Similarly to the case of nominal sets, an improvement of this recursion principle is possible, incorporating Barendregt’s variable convention. When interpreting syntax in semantic domains, my substitution-based recursor is easier to deploy than the nominal recursor. My results have been validated with the proof assistant Isabelle/HOL.

ABSTRACT. The propagation redundant (PR) proof system generalizes the resolution and resolution asymmetric tautology proof systems used by conflict-driven clause learning (CDCL) solvers. PR allows short proofs of unsatisfiability for some problems that are difficult for CDCL solvers. Previous attempts to automate PR clause learning used hand-crafted heuristics that work well on some highly-structured problems. For example, the solver SaDiCaL incorporates PR clause learning into the CDCL loop, but it cannot compete with modern CDCL solvers due to its fragile heuristics. We present PReLearn, a preprocessing technique that learns short PR clauses. Adding these clauses to a formula reduces the search space that the solver must explore. By performing PR clause learning as a preprocessing stage, PR clauses can be found efficiently without sacrificing the robustness of modern CDCL solvers. On a large number of SAT competition benchmarks we found that preprocessing with PReLearn significantly improves solver performance on both satisfiable and unsatisfiable formulas. PReLearn supports proof logging, giving a high level of confidence in the results.

ABSTRACT. The characterizing properties of a proof-theoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (one-dimensional) logics determined by (non-deterministic) logical matrices are known to be axiomatizable by analytic and possibly finite proof systems as soon as they turn out to satisfy a certain constraint of sufficient expressiveness. In this paper we introduce a recipe for cooking up a two-dimensional logical matrix (or B-matrix) by the combination of two (possibly partial) non-deterministic logical matrices. We will see that such a combination may result in B-matrices satisfying the property of sufficient expressiveness, even when the input matrices are not sufficiently expressive in isolate, and we will use this to show that one-dimensional logics that are not finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics, becoming, thus, finitely axiomatizable by the addition of an extra dimension. We will illustrate the said construction using a well-known logic of formal inconsistency called mCi. We will first prove that this logic is not finitely axiomatizable by a one-dimensional (generalized) Hilbert-style system. Then, taking advantage of a known 5-valued non-deterministic logical matrix for this logic, we will combine it with another one, conveniently chosen so as to give rise to a B-matrix that is axiomatized by a two-dimensional Hilbert-style system that is both finite and analytic.

ABSTRACT. Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such programs. The theory of arrays is widely supported but is not ideal, because the number of elements is fixed (determined by its index sort) and cannot be adjusted, which is a problem, given that the length of vectors often plays an important role when reasoning about vector programs. In this paper, we propose reasoning about vectors using a theory of sequences. We introduce the theory, propose a basic calculus adapted from one for the theory of strings, and extend it to efficiently handle common vector operations. We prove that our calculus is sound and show how to construct a model when it terminates with a saturated configuration. Finally, we describe an implementation of the calculus in cvc5 and demonstrate its efficacy by evaluating it on verification conditions for smart contracts and benchmarks derived from existing array benchmarks.

ABSTRACT. We discuss the results of our work on heuristics for generating minimal synthetic tableaux. We present this proof method for classical propositional logic and its implementation in Haskell. Based on mathematical insights and exploratory data analysis we defined a heuristics that allows to build a tableau of optimal or nearly optimal size. The proposed heuristics has been first tested on a data set with over 200 thousand of short formulas (length 12), then on a number of longer formulas (9 hundred of formulas of length 23). We describe the results of data analysis and examine some tendencies. We also confront our approach with the pigeonhole principle.

ABSTRACT. Treating a saturation-based automatic theorem prover (ATP) as a Las Vegas randomized algorithm is a way to illuminate the chaotic nature of proof search and make it amenable to study by probabilistic tools. On a series of experiments with the ATP Vampire, the paper showcases some implications of this perspective for prover evaluation.

ABSTRACT. Our goal is to develop a logic-based component for hybrid – machine learning plus logic – commonsense question answering systems. The paper presents an implementation GK of default logic for handling rules with exceptions in unrestricted first order knowledge bases. GK is built on top of our existing automated reasoning system with confidence calculation capabilities. To overcome the problem of undecidability of checking potential exceptions, GK performs delayed recursive checks with diminishing time limits. These are combined with the taxonomy-based priorities for defaults and numerical confidences.

ABSTRACT. We propose generalizations of reduction pairs, well-established techniques for proving termination of term rewriting, in order to prove unsatisfiability of reachability (infeasibility) in plain and conditional term rewriting. We adapt the weighted path order, a merger of the Knuth-Bendix order and the lexicographic path order, into the proposed framework. The proposed approach is implemented in the termination prover NaTT, and the strength of our approach is demonstrated through examples and experiments.

ABSTRACT. To give concise explanations for a conclusion obtained by reasoning over ontologies, justifications have been proposed as minimal subsets of an ontology that entail the given conclusion. Even though computing one justification can be done in polynomial time for tractable Description Logics such as EL+, computing all justifications is complicated and often challenging for real-world ontologies. In this paper, based on a graph representation of EL+-ontologies, we propose a new set of inference rules (called H-rules) and take advantage of them for providing a new method of computing all justifications for a given conclusion. The advantage of our setting is that most of the time, it reduces the number of inferences (generated by H-rules) required to derive a given conclusion. This accelerates the enumeration of justifications relying on these inferences. We validate our approach by running real-world ontology experiments. Our graph-based approach outperforms PULi, the state-of-the-art algorithm, in most of cases.