Bachmair’s and Ganzinger’s abstract redundancy concept for the Superposition Calculus justifies almost all operations that are used in superposition provers to delete or simplify clauses, and thus to keep the clause set manageable. Typical ...$$$$$$

Automated reasoning is a key research area of Artificial Intelligence (AI) and has attracted much greater attention in recent years due to the demands of trustworthy AI, where binary resolution inference rule based first-order automated reasoning ...

We present an automatic theorem prover for projective incidence geometry. This prover does not consider coordinates. Instead, it follows a combinatorial approach based on the concept of rank. This allows to deal only with sets of points and to ...

This paper reports on the industrial use of our formal-method based interlocking verification tool, called SafeCap, and on what we needed to change in SafeCap as a result of our experience in applying it to a large number of commercial signalling ...

This work describes a new version of a previously published Python package — gym-saturation: a collection of OpenAI Gym environments for guiding saturation-style provers based on the given clause algorithm with reinforcement learning. We ...

This paper describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to higher-order logic in the TPTP language using ...

Parikh-collinear morphisms have recently received a lot of attention. They are defined by the property that the Parikh vectors of the images of letters are collinear. We first show that any fixed point of such a morphism is automatic. Consequently,...$\mathrm{}\mathrm{}$$\mathrm{}\mathrm{}$

Verification of hardware-based cryptographic accelerators connects a low-level RTL implementation to the abstract algorithm itself; generally, the more optimized for performance an accelerator is, the more challenging its verification. This paper ...

AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying ...

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, Automated Theorem Proving (ATP) systems. CASC-J11 was the twenty-seventh competition in the CASC series. Twenty-four ATP systems competed in the various ...

In contrast to common automated theorem proving approaches, in which the search space is a set of some formulae and what is sought is again a (goal) formula, we propose an approach based on searching for a proof (of a given length) as a whole. ...

A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of ...$$

In his regular column in the AAR Newsletter, Larry Wos typically posed challenges to the automated reasoning community. Some of these challenges concern general research objectives, but several of them concern specific problems relevant to his own ...

We report on using logic software in a novel course-format for an undergraduate logic course for students in computer science or artificial intelligence. Although being designed as the students’ basic introduction to the field of logic, the course ...

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 ...

A strategy schedule allocates time to proof strategies that are used in sequence in a theorem prover. We employ Bayesian statistics to propose alternative sequences for the strategy schedule in each proof attempt. Tested on the TPTP problem ...

In recent years we have seen a number of satisfiability solvers emerge in the world of fuzzy propositional logics. However, only a few of them can solve product logic problems with the continuous product t-norm. The existing solvers may be ...$\mathrm{}$

Axiom selection is a task that selects the most likely useful axioms from a large-scale axiom set for proving a given conjecture. Existing axiom selection methods either solely take shallow symbols into account or strongly dependent on previous ...

We present a number of alternative ways of handling transitive binary relations that commonly occur in first-order problems, in particular equivalence relations, total orders, and transitive relations in general. We show how such relations can be ...

Human-centered automated proof search aims to capture structures of ordinary mathematical proofs and discover human strategies that are used (implicitly) in their construction. We analyze the ways of two theorem provers for approaching that goal. ...