Abstract. SAT solving techniques are used in many automated reasoning engines. This talk gives an overview on recent developments in practical aspects of SAT solver development. Beside improvements of the basic conflict driven clause learning (CDCL) algorithm, we also discuss improving and integrating advanced preprocessing techniques as inprocessing during search. The talk concludes with a brief overview on current trends in parallelizing SAT. |
Abstract. The Ontology Web Language (OWL) has received considerable traction recently and is used in a number of industrial and practical applications. While decidable, all basic reasoning tasks for OWL are intractable (most of them are N2ExpTime-complete). Thus, in order to obtain a system capable of solving practically-relevant nontrivial problems, a number of theoretical and practical issues need to be resolved. In my talk I will present an overview of the techniques employed in HermiT, a state-of-the-art OWL reasoner developed at Oxford University. I will present the main ideas behind the hypertableau calculus and contrast them with the tableau calculi used in similar systems. Furthermore, I will discuss optimization techniques used in HermiT such as the blocking cache, individual reuse, and core blocking. Finally, I will discuss certain higher-level optimizations implemented on top of the basic calculus, such as the recently-developed optimized classification algorithm. |
Abstract. We announce a tool for mapping derivations produced by the E theorem
prover to Mizar proofs. Our mapping complements earlier work that
generates problems for automated theorem provers from Mizar inference
checking problems. We describe the tool, explain the mapping, and
show how we solved some of the difficulties that arise in mapping
proofs between different logical formalisms, even when they are based
on the same notion of logical consequence, as Mizar and E are (namely,
first-order classical logic with identity). |
Abstract. This extended abstract presents several new automated theorem proving systems for first-order modal logics and sketches their calculi and working principles. The abstract also summarizes the results of a recent comparative evaluation of these new provers. |
Abstract. SMT solvers use simplex-based decision procedures to solve decision problems whose formulas are quantifier-free and atoms are linear constraints over the rationals. State-of-art SMT solvers use rational (exact) simplex implementations, which have shown good performance for typical software, hardware or protocol verification problems over the years.
Yet, most other scientific and technical fields use (inexact) floating-point computations, which are deemed far more efficient than exact ones.
It is therefore tempting to use a floating-point simplex implementation inside an SMT solver, though special precautions must be taken to avoid unsoundness.
In this work, we describe experimental results, over common benchmarks (SMT-LIB) of the integration of a mature floating-point implementation of the simplex algorithm (GLPK) into an existing SMT solver (OpenSMT).
We investigate whether commonly cited reasons for and against the use of floating-point truly apply to real cases from verification problems. |
Abstract. We investigate automated reasoning techniques as a means of supporting authorization enforcement functions of security-aware workflow management systems. The aim of such support is that one may statically or dynamically guarantee the realizability of a workflow instance given the security constraints of the underlying workflow specification. We develop two such automated reasoning methods and experimentally evaluate their suitability for giving such support. One method uses a propositional encoding of realizability implemented through binary decision diagrams, another method uses a linear-time temporal logic encoding implemented via bounded model checking. Preliminary experimental results identify issues of scalability and of balancing flexibility in task allocation with complexity of computing such allocations. |
Abstract. Recent work has shown that a technique using Binary Decision Diagrams (BDDs) to decide CTL and Int gives promising results. Based on this we explore how the method can be extended to other non-classical logics. In particular, we describe a putative method for deciding the modal mu-calculus using BDDs. |
Abstract. Workflow management systems (WfMSs) are useful tools for supporting enterprise information systems. Such systems must ensure compliance with guidelines and regulations. While formal verification techniques can be used in the development stages to help ensure behavioral properties of many systems, these techniques are generally not available in workflow tools. We present a framework which models workflows using Petri nets and translates the model to a tableau style model checker. The model checker uses the recently introduced one-pass tableau algorithm and delivers enhanced performance over traditional two-pass strategies in practical applications. A failed tableau will generate a counter model which can aid in debugging. We present a case study involving a health services delivery program, and verify properties written in Computation Tree Logic (CTL). The algorithm can be easily modified to accomodate other specification languages such as timed CTL, logics of beliefs, desires and intentions, temporal description logic, first order logic, and others. |
Abstract. This paper reports our initial experiments with
using external ATP and premise selection methods
on some corpora built with the HOL Light system.
The testing is done in three different settings,
corresponding to those used earlier for evaluating
such methods on the Mizar/MML corpus.
This is intended to provide the first estimate about
the usefulness of such external reasoning and AI systems for
solving problems over HOL Light and its libraries. |
Abstract. Mathematical textbooks typically present only one proof for most of the theorems. However, there are infinitely many proofs for each theorem in first-order logic, and mathematicians are often aware of (and even invent new) important alternative proofs and use such knowledge for (lateral) thinking about new problems.
In this paper we start exploring how the explicit knowledge of multiple (human and ATP) proofs of the same theorem can be used in learning-based premise selection algorithms in large-theory mathematics.
Several methods and their combinations are defined, and their effect on the ATP performance is evaluated on the MPTP2078 large-theory benchmark.
Our first findings are that the proofs used for learning significantly influence the number of problems solved, and that the quality of the proofs is more important than the quantity. |
Abstract. The efficiency of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary nature
of higher-order unification algorithms, which requires the integration of unification within the calculus and results in a non-efficient search for refutations.
We present a modification of the constrained resolution calculus (Huet'72) which uses an eager unification algorithm while retaining completeness. The
algorithm is complete with regard to bounded unification only, which for many cases, does not pose a problem in practice. |
Abstract. We present some parallelization techniques for the Model Evolution (ME) calculus,
an instantiation-based calculus that lifts the DPLL procedure
to first-order clause logic.
Specifically, we consider a restriction of ME to the EPR fragment
of clause logic for which the calculus is a decision procedure.
The main operations in ME's proof procedures, namely clause instantiation
and candidate literal generation, offer opportunities for MapReduce-style
parallelization.
This term/clause-level parallelization is largely orthogonal to the sort
of search-level parallelization performed by portfolio approaches.
We describe a hybrid parallel proof procedure for the restricted calculus
that exploits parallelism at both levels to synergistic effect.
The calculus and the proof procedure have been implemented in
a new solver for EPR formulas.
Our initial experimental results show that our term/clause-level parallelization
alone is effective in reducing runtime and can be combined
with a portfolio-based approach to maximize performance. |
Abstract. This paper presents two tableau provers for deciding interrogative-epistemic logics. They are both based on a tableau calculus generated using a recently introduced tableau synthesis framework. We have implemented the calculus using two approaches, namely Mettel2 and Qtab Here, we describe and compare these different approaches of implementing a tableau procedure. |
Abstract. Conflict-driven clause learning is currently the most efficient complete algorithm for satisfiability solving. However, a conflict-directed backtrack deletes potentially large portions of the current assignment that have no direct relation with the conflict. In this paper, we show that the CDCL algorithm can be generalized with a partial ordering on decision levels. This allows keeping levels that would otherwise be undone during backtracking under the usual total ordering. We implement partial ordering CDCL in a state-of-the-art CDCL solver and show that it significantly ameliorates satisfiability solving on some series of benchmarks. |
Abstract. We present the tool qbf2epr which translates quantified Boolean formulas (QBF) to
formulas in effectively propositional logic (EPR). The decision problem of QBF is the
prototypical problem for PSPACE, whereas EPR is NEXPTIME-complete. Thus QBF is
embedded in a formalism, which is potentially more succinct. The motivation for this workis twofold. On the one hand, our tool generates challenging benchmarks for EPR solvers.
On the other hand, we are interested in how EPR solvers perform compared to QBF solvers and if there are techniques implemented in EPR solvers which would also be valuable in QBF solvers and vice versa. |
Abstract. This paper introduces MetTeL2, a tableau prover generator producing Java code from the specifications of a logical syntax and a tableau calculus. It is intended to provide an easy to use system for non-technical users and allow technical users to extend the generated implementations. |
Abstract. In this paper we develop a sound, complete and terminating superposition calculus
plus a query answering calculus for the BSH-Y2 fragment of the
Bernays-Schoenfinkel Horn class of first-order logic.
BSH-Y2 can be used to represent expressive ontologies.
In addition to checking consistency, our calculus supports query answering
for queries with arbitrary quantifier alternations.
Experiments on BSH-Y2 (fragments) of several large ontologies show that our
approach advances the state of the art. |
