Abstract The Neuman-Stubblebine key exchange protocol is formalized in first-order logic
and analyzed by the automated theorem prover Spass. In addition to the analysis, we …

In this abstract we describe version 1.1 of the theorem prover Vampire. We give a general
description and comment on Vampire's original features and differences with the previously …

Connection calculi benefit from a goal-oriented proof search, but are in general not proof
confluent. A substantial amount of backtracking is required, which significantly affects the …

Logisches Schließen hilft den Menschen unter anderem beim Lösen von Problemen, durch
vorhandenes Wissen kann neues hergeleitet werden. Wir benutzen in unserem Leben eine …

The DPLL procedure is the basis of some of the most successful propositional satisfiability
solvers to date. Although originally devised as a proof-procedure for first-order logic, it has …

FDPLL is a directly lifted version of the well-known Davis-Putnam-Logeman-Loveland
(DPLL) procedure. While DPLL is based on a splitting rule for case analysis wrt. ground and …

This paper presents a technique for automated theorem proving with free variable tableaux
that does not require backtracking. Most existing automated proof procedures using free …

This paper presents a taxonomy of parallel theorem-proving methods based on the control
of search (eg, master–slaves versus peer processes), the granularity of parallelism (eg, fine …

Automatic reasoning tools play an important role when developing provably correct
software. Both main approaches, program verification and program synthesis employ …

This article is a tribute to the scientific legacy of automated reasoning pioneer and JAR
founder Lawrence T.(Larry) Wos. Larry's main technical contributions were the set-of-support …