PAAR-2014: Papers with Abstracts

Abstract. In 1994,
Bachmair, Ganzinger, and Waldmann introduced the hierarchical
superposition calculus as a generalization of the superposition
calculus for black-box style theory reasoning.
Their calculus works in a framework of hierarchic specifications.
It tries to prove the
unsatisfiability of a set of clauses with respect to interpretations
that extend a background model such as the integers with linear arithmetic
conservatively, that is, without
identifying distinct elements of old sorts ("confusion") and without
adding new elements to old sorts ("junk").
We show how the calculus can be improved,
report on practical experiments,
and present a new completeness result for
non-compact classes of background models
(i.e., linear integer or rational arithmetic restricted to
standard models).

Abstract. Many Automated Theorem Prover (ATP) systems for different logics, and
translators for translating different logics from one to another, have
been developed and are now available.
Some logics are more expressive than others, and it is easier to express
problems in those logics.
On the other hand, the ATP systems for less expressive logics have been
under development for many years, and are more powerful and reliable.
There is a trade-off between expressivity of a logic, and the power and
reliability of the available ATP systems.
Translators and ATP systems can be combined to try to solve
a problem.
In this research, an experiment has been carried out to compare the
performance of difference combinations of translators and ATP systems.

Abstract. Generalised Model Finding (GMF) is a quantifier instantiation heuristic for the superposition calculus in the presence of interpreted theories with arbitrarily quantified free function symbols ranging into theory sorts.
The free function symbols are approximated by finite partial function graphs along with some simplifying assumptions which are iteratively refined.
Here we present an outline of the GMF approach, give an improvement
that addresses some of these and then present some
ideas for extending it with concepts from instantiation based theorem proving.

Abstract. We present in expository style the main ideas in SGGS, which stands for Semantically-Guided Goal-Sensitive theorem proving. SGGS uses sequences of constrained clauses to represent models, instance generation to go from a candidate model to the next, and resolution as well as other inferences to repair the model. SGGS is refutationally complete for first-order logic, DPLL-style model based, semantically guided, goal sensitive, and proof confluent, which appears to be a rare combination of features. In this paper we describe the core of SGGS in a narrative style, emphasizing ideas and trying to keep technicalities to a minimum, in order to advertise it to builders and users of theorem provers.

Abstract. We describe the design and implementation of Logtk, an OCaml library for writing automated reasoning tools that deal with (possibly typed) first-order logic. The library provides data structures and algorithms to represent terms, formulas, substitutions, perform unification, index terms, parse problems, as well as a few tools to demonstrate itsuse. It is the basis of a full-fledged superposition prover.

Abstract. This paper presents BEAGLE TAC, a HOL4 tactic for using Beagle as an external ATP for
discharging HOL4 goals. We implement a translation of the higher-order goals to the TFA
format of TPTP and add trace output to Beagle to reconstruct the intermediate steps derived
by the ATP in HOL4. Our translation combines the characteristics of existing successful
translations from HOL to FOL and SMT-LIB, however we needed to adapt certain stages
of the translation in order to benefit form the expressivity of the TFA format and the power
of Beagle. In our initial experiments, we demonstrate that our system can prove, without
any arithmetic lemmas, 81% of the goals solved by Metis.

Abstract. Machine Learner for Automated Reasoning (MaLARea) is a learning and
reasoning system for proving in large formal libraries where
thousands of theorems are available when attacking a new
conjecture, and a large number of related problems and proofs can be used to
learn specific theorem-proving knowledge. The last version of the
system has by a large margin won the 2013 CASC LTB competition. This
paper describes the motivation behind the methods used in MaLARea,
discusses the general approach and the issues arising in evaluation
of such system, and describes the Mizar@Turing100 and CASC'24
versions of MaLARea.

Abstract. The TPTP (Thousands of Problems for Theorem Provers) World is a well established infrastructure for Automated Theorem Proving (ATP). In the context of the TPTP World, the TPTP Process Instruction (TPI) language provides capabilities to input, output and organize logical formulae, and control the execution of ATP systems. This paper reviews the TPI language, describes a shell interpreter for the language, and demonstrates their use in theorem proving.

Abstract. Razor is a model-finder for first-order theories presented
geometric form; geometric logic is a variant of first-order logic
that focuses on ``observable'' properties. An important guiding
principle of Razor is that it be accessible to users who are
not necessarily expert in formal methods; application areas
include software design, analysis of security protocols and
policies, and configuration management.

A core functionality of the tool is that it supports
exploration of the space of models of a given input theory,
as well as presentation of provenance information about the
elements and facts of a model. The crucial mathematical tool is
the ordering relation on models determined by homomorphism, and
Razor prefers models that are minimal with respect to this
homomorphism-ordering.

Abstract. We describe an algorithm that generates prime implicates of equational clause sets without variables and function symbols. The procedure is based on constrained superposition rules, where constraints are used to store literals that are asserted as additional axioms (or hypotheses) during the proof search. This approach is sound and deductive-complete, and it is more ecient than previous algorithms based on conditional paramodulation. It is also more exible in the sense that it allows one to restrict the search space by imposing additional properties that the generated
implicates should satisfy (e.g., to ensure relevance).

Abstract. We present an extension of superposition that natively handles a polymorphic type system extended with type classes, thus eliminating the need for type encodings when used by an interactive theorem prover like Isabelle/HOL. We describe syntax, typing rules, semantics, the polymorphic superposition calculus and an evaluation on a problem set that is generated from Isabelle/HOL theories. Our evaluation shows that native polymorphic+typeclass performance compares favorably to monomorphisation, a highly efficient but incomplete way of dealing with polymorphism.