Predrag Janičić
email: janicic@matf.bg.ac.rs

Julien Narboux
email: narboux@unistra.fr

Theorem Proving as Constraint Solving with Coherent Logic

Keywords: Automated theorem proving, interactive theorem proving, constraint solving, coherent logic, SAT/SMT solving

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. Namely, a proof of a formula in a fixed logical setting can be encoded as a sequence of natural numbers meeting some conditions and a suitable constraint solver can find such sequence. The sequence can then be decoded giving a proof in the original theory language. This approach leads to several unique features, for instance, it can provide shortest proofs. In this paper, we focus on proofs in coherent logic, an expressive fragment of first-order logic, and on SAT and SMT solvers for solving sets of constraints, but the approach could be tried in other contexts as well. We implemented the proposed method and we present its features, perspectives and performances. One of the features of the implemented prover is that it can generate human understandable proofs in natural language and also machine verifiable proofs for the interactive prover Coq.

Introduction

The central task of automated theorem proving -proving a conjecture given some premises -can be pursued in a range of ways, all of which are some form of search. In almost all of them, the search space is a set of some formulae and what is sought is again a formula (often a contradiction). There is no assumption on the size of the proof, and the size of the proof is known only after the target formula has been found (if it has been found).

We propose a completely different approach: instead of searching for some formula, we propose searching for a proof as a whole. A (finite, fixed length) proof can be encoded, represented as a sequence of natural numbers or Boolean constants meeting some constraints. For given premises and a given conjecture, that representation yields a set of concrete constraints and solving them gives a needed proof. Hence, this approach can be called "theorem proving as constraint solving". The approach has some unique features, including yielding short and shortest possible proofs (in terms of the given axioms, without additional lemmas). It is often the case that we know there is some relatively short proof (or we may be interested in such proofs only), for instance, in development of mathematical theories. Then, we can focus on searching for a short proof, while the shortest proof can be especially appreciated. Another unique feature are hints: it can be easily required that some specific inference step or some specific axiom must be used within the proof (all other proving approaches, when they are provided with some axioms, may use them, but are not obliged to). Hints may be useful, for example, in the following context: given an informal proof of some theorem or fragments of a formal proof in some specific representation, we can use that information as hints for helping our system in reconstructing the concrete proof under consideration.

The approach could be tried for various logics and calculi -if one needs an automated theorem prover for some theory, he/she needs to specify only the notion of proof (and the way the proofs are mapped into sequences of natural numbers). We concentrate on coherent logic (CL), an expressive fragment of first-order logic. The absence of function symbols in CL allows a trivial encoding of matching of axiom arguments. CL proofs are easily transformed into formal proofs of interactive theorem provers. In addition, CL can serve well as a vehicle for readable proofs, its proofs are simple and natural, which is achieved by combining several natural deduction rules into one rule. CL proofs can also suitably serve as a basic for further post-processing so they can be more human-style.

We implemented the proposed approach and here we present that implementation too. We translate the proof constraints into propositional logic or into some decidable theories of first-order logic (such as linear arithmetic), and solve them using SAT and SMT solvers. From the obtained models, we generate proofs that are machine verifiable or that are given in a natural language form. The approach and the system we present can be subject to different improvements and optimisations. Hence, we don't see this paper as a final, but rather as a first step in this new direction of research.

Overview of the paper: In Section 2 we give some background information on coherent logic and on a constraint solver URSA. In Section 3 we present key ideas and techniques within the proposed approach, primarily how is a proof represented as a sequence of natural numbers. In Section 4 we present our prototype implementation. In Section 5 we present some evaluation results and some analysis of performance of our implementation. In Section 6 we discuss some features of the proposed approach and its implementation and some scenarios of usage. In Section 7 we briefly discuss related work. In Section 8 we discuss some possible directions for future work and in Section 9 we draw some final conclusions.

Background

We assume the reader is familiar with basic notions of automated theorem proving (ATP) and interactive theorem proving (ITP). In particular, we assume some basic knowledge of SAT and SMT solvers [START_REF]Handbook of Satisfiability[END_REF], of the interactive provers Coq [START_REF]The Coq development team[END_REF] and Isabelle [START_REF] Nipkow | Isabelle HOL: a Proof Assistant for Higher-Order Logic[END_REF], and their interconnections [START_REF] Böhme | Fast LCF-Style Proof Reconstruction for Z3[END_REF].

Coherent Logic. A formula of first-order logic is said to be coherent if it has the following form:

A 0 ( x) ∧ . . . ∧ A n-1 ( x) ⇒ ∃ y(B 0 ( x, y) ∨ . . . ∨ B m-1 ( x, y))
where universal closure is assumed, and where 0 ≤ n, 0 ≤ m, x denotes a sequence of variables x 0 , x 2 , . . . , x k-1 (0 ≤ k), A i (for 0 ≤ i ≤ n -1) denotes an atomic formula (involving zero or more variables from x), y denotes a sequence of variables y 0 , y 2 , . . . , y l-1 (0 ≤ l), and B j (for 0 ≤ j ≤ m -1) denotes a conjunction of atomic formulae (involving zero or more of the variables from x and y). If n = 0, then the left hand side of the implication is assumed to be . If m = 0, then the right hand side of the implication is assumed to be ⊥ . There are no function symbols with arity greater than zero. Coherent formulae do not involve the negation connectives. A coherent theory is a set of sentences, axiomatised by coherent formulae, and closed under derivability. 1 A number of theories and theorems can be formulated directly and simply in coherent logic (CL). Several authors independently point to CL (or rules similar to those of CL) as suitable for expressing (sometimes -also automating) significant portions of mathematics [START_REF] Avigad | A Formal System for Euclid's Elements[END_REF][START_REF] Ganesalingam | A fully automatic problem solver with human-style output[END_REF]. In contrast to resolution-based theorem proving, in forward reasoning for CL, the conjecture being proved is kept unchanged and proved without using refutation, Skolemization and clausal form. Thanks to this, CL is suitable for producing readable synthetic proofs [START_REF] Bezem | Automating Coherent Logic[END_REF] with "structure of ordinary mathematical arguments better retained" [START_REF] Dyckhoff | Geometrization of first-order logic[END_REF] and also for producing machine verifiable proofs.

Every first-order theory has a coherent conservative extension [START_REF] Dyckhoff | Geometrization of first-order logic[END_REF][START_REF] Polonsky | Proofs, Types and Lambda Calculus[END_REF], i.e., any first-order theory can be translated into CL, possibly with additional predicate symbols. This translation process is called "coherentisation" or, sometimes, "geometrisation" [START_REF] Dyckhoff | Geometrization of first-order logic[END_REF]. Translation of FOL formulae into CL involves elimination of the negation connectives: negations can be kept in place and new predicates symbols for corresponding sub-formula have to be introduced, or negations can be pushed down to atomic formulae [START_REF] Polonsky | Proofs, Types and Lambda Calculus[END_REF]. In the latter case, for every predicate symbol R (that appears in negated form), a new symbol R is introduced that stands for ¬R, and the following axioms are introduced: ∀ x(R( x) ∧ R( x) ⇒ ⊥), ∀ x(R( x) ∨ R( x)). In order to enable more efficient proving, some advanced translation techniques are used. Elimination of function symbols, sometimes called anti Skolemization, is also done by introducing additional predicate symbols [START_REF] De | Geometric Resolution: A Proof Procedure Based on Finite Model Search[END_REF].

If a CL formula can be classically proved from a set of CL formulae, then it can also be intuitionistically proved from that set (this statement is known as the first-order Barr's Theorem [START_REF] Dyckhoff | Geometrization of first-order logic[END_REF]). However, translation from FOL to CL is not necessarily constructive.

The problem of provability in CL is semi-decidable. CL admits a simple proof system, a sequent-based variant is as follows [START_REF] Stojanović | A Vernacular for Coherent Logic[END_REF]: QEDas (assumption)

Γ, ⊥ P QEDefq (ex falso quodlibet)

In the rules given above, it is assumed: ax is a formula A 0 ( x) ∧ . . . ∧ A n-1 ( x) ⇒ ∃ y(B 0 ( x, y) ∨ . . . ∨ B m-1 ( x, y)); 2 a, b, c denote sequences of constants (possibly of length zero); in the rule MP (extended modus ponens), b are fresh constants; x and y denote sequences of variables (possibly of length zero); A i ( x) (B i ( x, y)) have no free variables other than from x (and y); A i ( a) are ground atomic formulae; B i ( a, b) and B i ( c) are conjunctions of ground atomic formulae; Φ denotes the list of conjuncts in Φ if Φ is conjunction, and otherwise Φ itself. In the proving process, the rules are read from bottom to top, i.e., by a rule application one gets the contents (new subgoals) above the line. 3 For a set of coherent axioms AX and the statement A 0 ( x) ∧ . . . ∧ A n-1 ( x) ⇒ ∃ y(B 0 ( x, y) ∨ . . . ∨ B m-1 ( x, y)) to be proved, within the above proof system one has to derive the following sequent (where a denotes a sequence of new symbols of constants): AX , A 0 ( a), . . . , A n-1 ( a) ∃ y(B 0 ( a, y) ∨ . . . ∨ B m-1 ( a, y)).

Notice that in the above proof system case split may occur only at the end of a (sub)proof. However, it is not a substantial restriction: any proof with unrestricted use of case split can be transformed to a proof in the above system. ∀x (p(x) ⇒ r(x)) Using the above rule system, the theorem can be proved as follows: ax1, ax2, p(a), r(a) r(a) QEDas ax1, ax2, p(a), q(a), ⊥ r(a) QEDefq ax1, ax2, p(a), q(a) r(a) MP(ax2) ax1, ax2, p(a), r(a) ∨ q(a) r(a) QEDcs ax1, ax2, p(a) r(a)

MP(ax1)

The same proof can be given in a forward manner, in a natural language form (this proof was generated by our prover, described in the rest of the paper):

Consider an arbitrary a such that: p(a). It should be proved that r(a).

1. r(a) ∨ q(a) (by MP, from p(a) using axiom ax1; instantiation: X → a)

2. Case r(a): 3. Proved by assumption! (by QEDas) 4. Case q(a):

5. ⊥ (by MP, from q(a) using axiom ax2; instantiation: X → a) 6. Contradiction! (by QEDefq) 7. Proved by case split! (by QEDcs, by r(a), q(a))

The above, forward directed form will be used for modelling proofs in the rest of the paper.

Constraint programming systems URSA. The constraint solving system URSA4 [START_REF] Janičić | URSA: A System for Uniform Reduction to SAT[END_REF] is based on reduction to the propositional satisfiability problem (SAT). In URSA, the problem is specified in a language which is imperative and similar to C, but at the same time, is declarative, as the user does not have to provide a solving mechanism for the given problem. URSA allows two types of variables: natural numbers (with names beginning with n, e.g., nX) and Booleans (with names beginning with b, e.g., bX), with a wide range of C-like operators (arithmetic, relational, logical, and bitwise). Variables can have concrete (ground) or symbolic values (in which case, they are represented by vectors of propositional formulae). There is support for procedures and there are control-flow structures (in the style of C). Loops must be with known bounds and there is no if-else statement, but only ite expressions (corresponding to ?: in C). An URSA specification is symbolically executed and the given constraint corresponds to a propositional formula. It is then transformed into CNF and passed to one of the underlying SAT solvers. If this formula is satisfiable, the system can return all its models.

Proof Encoding for Coherent Logic and Proof Search

In this section we discuss how a proof in a fragment of CL can be represented as a sequence of natural numbers. The basic idea of the encoding is to encode individual proof steps as fixed-size sequences of numbers with appropriate conditions, and to add conditions constraining the global proof structure. Individual proof steps are represented, among others, by sequences of numbers that correspond to facts derived in that step, corresponding inference rules and, possibly, axioms along with instantiations used. We skip some details, unsubstantial ideas or tricks in order to have the central ideas clearer. A number of aspects of this representation (i.e., of the proof encoding), can be defined in some other way, but we don't discuss all alternatives. Also, there are some redundancies in the encoding, introduced for more convenient representation and proof decoding.

The proposed approach can be applied to the full CL, but it is simpler and more convenient to apply it to its fragment that we call CL2. This restriction is not substantial. Indeed, for proving any formula in CL it is sufficient to prove a corresponding formula in CL2. CL formulae are of the form (universally closed):

A 0 ( x) ∧ . . . ∧ A n-1 ( x) ⇒ ∃ y(B 0 ( x, y) ∨ . . . ∨ B m-1 ( x, y))
while CL2 formulae meet the following restrictions:

m = 1 or m = 2; -each formula B i consists of only one conjunct.

From CL to CL2 and Back

Transformation from CL to CL2 is based on the following steps (universal closure is assumed for all formulae):5 -An axiom

P ⇒ ∃ y(Q ∨ (C 0 ∧ C 1 ∧ . . . ∧ C k-1 ) ∨ R), if k > 1
, is replaced by the following axiom:

P ⇒ ∃ y(Q ∨ C 0,1,...,k-1 ∨ R),
using a shorthand with a new predicate symbol:

C 0,1,...,k-1 ≡ C 0 ∧ C 1 ∧ . . . ∧ C k-1 (C 0,1,...,k-1 involves all variables that occur in C 0 , C 1 , . . ., C k-1
), and requiring additional axioms:

C 0,1,...,k-1 ⇒ C 0 C 0,1,...,k-1 ⇒ C 1 . . . C 0,1,...,k-1 ⇒ C k-1 -An axiom P ⇒ ∃ y(Q 0 ∨ Q 1 ∨ . . . ∨ Q k-1 ), if k > 2,
and where all Q i are atomic formulae, is replaced by the following axiom:

6 P ⇒ ∃ y(Q 0,1,...,k-2 ∨ Q k-1 )
using shorthands with new predicate symbols:

Q 0,1 ≡ Q 0 ∨ Q 1 Q 0,1,2 ≡ Q 0,1 ∨ Q 2 . . . Q 0,1,...,k-2 ≡ Q 0,1,...,k-3 ∨ Q k-2
(Q 0,1,...,i involves all variables that occur in Q 1,2,...,i-1 and Q i ), and requiring additional axioms:

Q 0,1 ⇒ Q 0 ∨ Q 1 Q 0,1,2 ⇒ Q 0,1 ∨ Q 2 . . . Q 0,1,...,k-2 ⇒ Q 0,1,...,k-3 ∨ Q k-2
-If the conjecture is of the form

P ⇒ C 0 ∧ C 1 ∧ . . . ∧ C k-1 ,
then it is replaced by a sequence of conjectures

P ⇒ C i , for 0 ≤ i ≤ k -1.
-If the conjecture is of the form:

P ⇒ ∃ y(Q ∨ (C 0 ∧ C 1 ∧ . . . ∧ C k-1 ) ∨ R), if k > 1,
it is replaced by the following conjecture:

P ⇒ ∃ y(Q ∨ C 0,1,...,k-1 ∨ R)
using a shorthand with a new predicate symbol:

C 0,1,...,k-1 ≡ C 0 ∧ C 1 ∧ . . . ∧ C k-1
(C 0,1,...,k-1 involves all variables that occur in C 0 , C 1 , . . ., C k-1 ), and requiring additional axioms: 6 Transformation based on binary cuts of sets of formula would lead to a smaller set of new short-hands and additional axioms -of size O(log k) instead of O(k). However, the size of disjunctions in real-world examples is usually not too large, so we keep the simple version and will experiment with the second one in the future.

C 0 ∧ C 1 ∧ . . . ∧ C k-1 ⇒ C 0,1,...,k-1
-If the conjecture is of the form

P ⇒ ∃ y(Q 0 ∨ Q 1 ∨ . . . ∨ Q k-1 ), if k > 2,
and where all Q i are atomic formulae, it is replaced by the following conjecture:

P ⇒ ∃ y(Q 0,1,...,k-1 ) using shorthands with new predicate symbols:

Q 0,1,...,k-1 ≡ Q 0 ∨ Q 1 ∨ . . . ∨ Q k-1 (Q 0,1,...,k-1 involves all variables that occur in Q 0 , Q 1 , . . ., Q k-1
), and requiring additional axioms:

Q 0 ⇒ Q 0,1,...,k-1 Q 1 ⇒ Q 0,1,...,k-1 . . . Q k-1 ⇒ Q 0,1,...,k-1
The above rules are applied in iterations until all axioms and the conjecture are in CL2 form. It is obvious that this process terminates.

Example 2 The axiom:

∀x (p(x) ⇒ (q(x) ∨ (r(x) ∧ s(x)) ∨ t(x)))
is replaced by the following axioms: ∀x (p(x) ⇒ (q or r and s(x) ∨ t(x))) ∀x (q or r and s(x)(x) ⇒ (q(x) ∨ r and s(x)) ∀x (r and s(x) ⇒ r(x)) ∀x (r and s(x) ⇒ s(x))

The conjecture: A similar transformation could be used to reduce the number of premises in each axiom to at most two (but we do not use it).

∀x∃y (a(x) ⇒ (b(x, y) ∨ (c(y) ∧ d(y)) ∨ e(y))))) is
A theory T obtained this way from a CL theory T is its conservative extension. Given a proof in CL2, it is easy to obtain a corresponding proof in CL: all introduced predicate symbols have to be eliminated, i.e., defined expressions have to be replaced by their corresponding definitions in terms of the original signature. This means, however, that not all assumption steps (in the final proof) will hold only facts, but possibly also disjunctions or conjunctions.

As said in Section 2, in translation from FOL to CL, for every predicate symbol R that appears in negated form, a new symbol R is introduced that stands for ¬R. As a final step in constructing a proof, we can translate R back to ¬R (keeping the axioms ∀ x(R( x) ∧ ¬R( x) ⇒ ⊥), and ∀ x(R( x) ∨ ¬R( x))).

Intro

As mentioned in Section 2, given the conjecture (the atom B 1 ( x, y) may be absent):

A 0 ( x) ∧ . . . ∧ A n-1 ( x) ⇒ ∃ y(B 0 ( x, y) ∨ B 1 ( x, y))
, new constants a are introduced and the proving task becomes the task of checking whether it holds that:

A 0 ( a), . . . , A n-1 ( a) ∃ y(B 0 ( a, y) ∨ B 1 ( a, y))

Kinds of Proof Steps

Following the definitions of CL and CL2, a class of CL2 proofs can be represented in the following simple way (there are zero or more assumptions -As, MP is used zero or more times, QEDcs involves two other objects Proof):

Proof ::= As * MP * QEDcs Proof 2 | QEDas | QEDefq
Therefore, any CL2 proof can be represented as a sequence of steps and each step is one of the following:

Assumption : This step contains a fact A( a), introduced by the conjecture formulation or by cases in proofs by cases. MP : An axiom (universally quantified) This step opens the first case consideration (i.e., the first subproof) and it introduces the assumption B 0 ( a, b). Without loss of generality, we impose the restriction that that MP step is the immediate previous step. It can be easily proved that this does not harm completeness. SecondCase : There is a preceding MP step with a conclusion

A 0 ( x) ∧ . . . ∧ A n-1 ( x) ⇒ ∃ y(B 0 ( x, y) ∨ . . . ∨ B m-1 ( x,
B 0 ( a, b) ∨ B 1 ( a, b),
and a corresponding FirstCase completed in the previous proof step. This step opens the second case consideration (i.e., the second subproof) and it introduces the assumption B 1 ( a, b). QEDbyCases : There is a preceding MP step with a conclusion B 0 ( a, b) ∨ B 1 ( a, b) and both cases have been completed (in the previous step). This step closes the proof by cases. QEDbyAssumption : The goal statement is present in the assumptions or is derived in the previous step. QEDbyEFQ : If ⊥ has been derived in the previous step, then the goal statement has been proved as well.

Axioms and Conjecture Representation

We assume that all the given axioms are in the fragment CL2. The axioms are ordered and each is assigned an ordinal number. The same holds for the predicate symbols and for the symbols of constants (from the original signature and those introduced later, as fresh constants). (The symbols ⊥ and as predicate symbols of arity 0 may be assigned values 0 and 1). An axiom A 0 ( x) ∧ . . . ∧ A n-1 ( x) ⇒ ∃ y(B 0 ( x, y) ∨ B 1 ( x, y)) (universal closure is assumed) is represented by the following pieces of information:

the ordinal number; -the number of universal quantifiers; -the number of existential quantifiers; -the number of premises (i.e., the number n); -a flag, true if the axiom is branching (i.e., if there is an atom B 1 ), false, otherwise; -the ordinal numbers of predicates symbols occurring in the axiom (respectively in the premises and the goal), i.e., the original numbers of dominant symbols in A 0 , . . . , A n-1 , B 0 , B 1 ; -a flag saying whether a certain argument in an atomic formulae is a constant symbol, and if yes, the ordinal number of that constant symbol; -the mapping between variables within the atomic formulae and the quantifiers.

All of the above values can be represented by natural numbers. We use zerobased counting (like in C/C++), for a more compact representation.

Example 3 Consider the axiom ax1: ∀x (p(x) ⇒ r(x) ∨ q(x)) from Example 1. Let us assume that the predicate symbols and their negated versions p, ¬p, r, ¬r, q, ¬q are represented by the numbers 2, 3, 4, 5, 6, 7, and the constant a is represented by 0. Then, the axiom is represented by the following values:

the ordinal number is 1; -the number of universal quantifiers is 1; -the number of existential quantifiers is 0; -the number of premises is 1; -the axiom is branching; -the ordinal numbers of predicates symbols are 2, 4, 6; -no argument in the atomic formula is a constant; -each variable appearing in the atomic formula maps to the first quantified variable.

Proof Step Representation

The proof is represented as an ordered list of proof steps. The structure of the proof is encoded using some nesting information attached to each proof step. Encoding of proof steps is adjusted to a concrete conjecture to be proved: a maximal number of premises in the axioms is known, and a maximal arity of predicate symbols is known, so fixed-size slots are used for encoding each proof step. Each proof step is represented by the following values (not all are necessarily relevant for each step):

StepKind : one of the possible step kinds (see the list in Section 3.3); Contents : one or two atoms, represented by their predicate symbols and argument constants: P 0 (a 0 , ..., a k-1 ) and, possibly, P 1 (a 0 , ..., a l-1 ).

Nesting : a value that characterises the position of the step in the proof considered as a tree. The initial value is 1. Each MP step has the same nesting as its previous step. In a proof by cases, if the cases are introduced by a MP step with nesting n, then the FirstCase step has nesting 2n, the corresponding SecondCase step has nesting 2n + 1, and the corresponding QEDbyCases has nesting n. Goal : says whether the contents of the step s matches the goal (this is redundant information, but convenient for expressing conditions for some proof steps). In one proof, there may be several steps s for which Goal (s) is true.

The following pieces of information are relevant for MP steps only:

AxiomApplied : the ordinal number of the axiom used;

From values: the ordinal numbers of proof steps justifying premises of the axiom applied; Instantiation : the instantiation used (for instance, σ = [ x → a, y → b]). It is stored as a sequence of ordinal numbers of constants to which the quantified variables are mapped respectively. For axioms that introduce new constants, they map to new, unused natural numbers. Cases : says whether the used axiom is branching or not (this is redundant information, but convenient); Premises : says how many premises the axioms used has (this is redundant information, but convenient).

All of the above values can be represented by natural numbers (again, zerobased counting like in C/C++ is used). 1. r(a) ∨ q(a) (by MP, from p(a) using axiom ax1; instantiation: X → a)

2. Case r(a): 3. Proved by assumption! (by QEDas) 4. Case q(a):

5. ⊥ (by MP, from q(a) using axiom ax2; instantiation: X → a) 6. Contradiction! (by QEDefq) 7. Proved by case split! (by QEDcs, by r(a), q(a))

Its proof steps can be represented by the following numerical values, given that predicate symbols and their negated versions p, ¬p, r, ¬r, q, ¬q are represented by the numbers 2, 3, 4, 5, 6, 7, the constant a is represented by 0, and the information on StepKind and AxiomApplied is packed in one number, as explained in Section 4.2:

Goal Representation

Let us suppose that the task is to show (the atom B 1 may be absent):

A 0 ( a), . . . , A n-1 ( a) ∃ y(B 0 ( a, y) ∨ B 1 ( a, y)).
Then the goal, the formula ∃ y(B 0 ( a, y) ∨ B 1 ( a, y), is used to set constraints on the last possible proof step, i.e., on the MaxL -1-th step (recall that zero-based counting is used), where MaxL is the maximal proof length (a concrete number) that has to be provided. The goal is described similarly as other proof steps:

its StepKind is one of QEDbyAssumption , QEDbyCases , QEDbyEFQ ; -Contents (MaxL -1)(0) = B 0 ( a, y) (and possibly Contents (MaxL -1)(1) = B 1 ( a, y), if B 1 is present); the variables y as arguments have a special treatment; -Nesting (MaxL -1) equals 1; -Cases (MaxL -1) is true iff there is the atom B 1 , i.e., there is a disjunction in the goal).

A proof to be found may have a length L, less or equal MaxL, as ensured by constraints presented in Section 3.8.

Encoding of Proof Steps -Local Constraints

Let us express conditions that have to be met for a proof step of a particular kind. Let the length of the proof be L. It must hold that L ≤ MaxL, and for each proof step s (0 ≤ s < L) one of the following groups of conditions holds (i.e., each step has one of the listed step kinds). Notice that L is a symbolic, not a concrete value, so a check if 0 ≤ s < L is used as a constraint.

Assumption : Given the initial assumptions A 0 ( a), . . ., A n-1 ( a), they constitute the first n steps of the proof (they do not introduce any unknown), for s < n: Let us comment more on the encoding of the step kind FirstCase , for instance. The given constraints say that such proof step cannot be the very first proof step (i.e., the 0th step), that the previous step is a branching MP step, the step itself is not branching, and its contents is the same as the first atom of the previous step, while the nesting doubles.

Example 5 Consider again a proof from Example 4, and let us illustrate the above constraints on its two last steps. One step before the last one (6th step) has a step kind QEDbyEFQ . Indeed, 5 > 0 (recall that internally we use zero-based counting), the contents of its previous step is ⊥, the contents of this step (not shown in the presented proofs) is r(a), and its nesting is equal to the nesting of its previous step. The last step (7th step) has a step kind QEDbyCases . Indeed, 6 > 0, the contents of its previous step is r(a), the contents of this step (not shown in the presented proofs) is, again, r(a), the nesting of the previous step equals 3, hence it is odd, and finally, the nesting of this proof step equals (3-1)/2.

Encoding of Proof as a Whole -Global Constraints

The global constraints ensure that the global structure (most notably case splits) is correct and that the goal has been reached at the end of the proof. In the following, the proof length equals L (L is unknown, there is only a constraint 0 < L ≤ MaxL, where MaxL is the given, concrete maximal proof length). In all the rules, it must hold that 0 ≤ s < L:

1. Each proof step s is one of the defined step kinds; 2. If step s -1 is one of the QED steps, then Nesting (s -1) = Nesting (s); 3. If Cases (s -1) is true, then StepKind (s) = FirstCase ; 4. If s -1 is one of the QED steps and Nesting (s-1) is even, then StepKind (s) = SecondCase ; 5. If s -1 is one of the QED steps and Nesting (s -1) is odd, then StepKind (s) = QEDbyCases ; 6. Nesting (L -1) = 1; 7. The step L -1 is one of the QED steps; 8. Contents (L -1) = Contents (MaxL -1 ).

Notice that, without uninterpreted functions, a condition like Nesting (L-1) = 1 cannot be expressed directly because L is unknown. Instead, the constraint is constructed as a disjunction over all possible values of L.

Proof Search

Given some axioms, a conjecture, and a maximal proof length MaxL, a set of constraints (in variables ranging over natural numbers) that describe a proof of the conjecture can be constructed, as explained above. If the set of constraints is satisfiable, its model can be decoded into a concrete proof.

A proof search can be facilitated in the following way: first, a proof of length at most a is initially sought, and if there is no such proof, a proof of length at most a + b, a + 2b, a + 3b etc, is sought (in our implementation, there are default values for a and b, but also the user can set a and b, see Section 4.4). Such policy enables faster proof finding for simple theorems and still preserve completeness for more complex ones (while trying to introduce a small number of constraints). The search stops if a proof is found, or the maximal proof length has been reached, or if the available time has been spent.

Properties

Given a maximal proof length, the presented proving method is trivially terminating. In addition, even without a given maximal proof length, if the input statement is provable, and the method is applied for an increasing sequence of maximal proof lengths, this process is also terminating. Hence, one of the key issues for many proving paradigms -termination -is trivial for the presented approach. The form of axioms does not affect this -termination is trivially ensured also in the presence of axioms that may lead to non-terminating rewrite rules, like commutativity axioms.

The presented approach is sound: what is generated as a proof of the given conjecture is indeed its proof. The presented approach is complete in the following sense: if there is a CL2 proof of length ≤ MaxL of the given conjecture, it will be eventually found (assuming that the underlying SAT/SMT provers are complete). Even more, we can systematically increase MaxL (and the maximal nesting, if needed) and check if there is a proof of length ≤ MaxL. A CL2 formula is a consequence of the given axioms if and only if there is a MaxL such that there is a proof of length ≤ MaxL. This gives a semi-decision procedure for validity in CL2, as a by-product of the proposed approach. It can be extended to full FOL, since any first-order theory can be translated into CL2.

The above outlined features could be the subject of rigorous proofs and formalisation using an interactive prover and a reflexive approach, but at this, first stage we rather chose to use an approach based on certification of generated proofs using state-of-the-art ITP, instead of proving correctness and completeness of our prototype implementation. This approach has several advantages:

we can change the prover easily, without changing the proof checker and we do not need to write a new proof; -we can use efficient implementations, with optimisations which would be hard to verify; -we can choose the implementation language and we could use parallelisation and native computation (without the layers of abstraction/interpretation involved in a reflexive approach); -we can use external tools that we do not need to verify (SAT and SMT solvers) nor use certified versions 10 .

On the other hand, the drawback is that we cannot be completely sure that the encoding is correct, so our prover may possibly fail.

The complexity of the proposed approach is difficult to estimate. In terms of the number of constraints, the largest portion goes to describing MP steps. If there are A axioms, each of them with maximally p premises, and maximally a arguments, then the number of these constraints for the l + 1-th proof step can be bounded by A•a•l p . If MaxL is the maximal proof length, by summation for l = 0, . . . , MaxL-1, the number of these constraints belongs to O(A • a • MaxL p+1 ). However, it is very well known that the number of the constraints (in SAT or SMT) is not simply or directly related to the complexity of the solving phase. Thus, we will stick only to some experimental evaluation, rather than on theoretical worst-case or averagecase analysis (see Section 5). In practice, the encoding and decoding phases of the prover take negligible time compared to the SAT/SMT solving phase.

Extensions

We considered a number of extensions of the basic approach described above. Some of them were not beneficial, like describing constraints in an incremental manner (for instance, using conditions for a proof step in conditions for the subsequent proof step), using integrated support for equality axioms (instead of external, individual axioms for each predicate symbol), using integrated support for excluded middle axioms (instead of external, individual axioms for each predicate symbol), etc. In the following, we describe the extensions that had positive impact on efficiency of the approach.

Symmetry Breaking. As in many other kinds of constraint problems, symmetry breaking can be exploited in the presented approach. Symmetry breaking can lead to more concise constraints and to a more efficient solving phase. However, some care needs to be taken that additional constraints do not disturb the search space, in our context, that is, do not eliminate some proofs of interests.

One of the additional constraints that we use for symmetry breaking imposes a partial ordering of proof steps and reduces a number of possible proofs: if two MP steps s and s are such that s + 1 = s , Nesting (s) = Nesting (s ), and s does not use s, then it must hold that:

Premises (s ) > Premises (s) or (Premises (s ) = Premises (s) and AxiomApplied (s ) ≥ AxiomApplied (s)).

Axioms Inlining. We call the axioms of the following forms (universally closed, x is a sequence of variables, A( x) and B( x) denote atomic formulae):

B( x) A( x) ⇒ B( x)
simple axioms. In one extension of our basic approach, these axioms are not to be applied through MP steps. Instead, in a MP step with a non-simple axiom applied, premises of the axiom can be justified not only by previous proof steps, but also by suitable, "inline" applications of simple axioms. This makes constraints for MP steps more complex but, on the other hand, enables shorter proofs.

Example 6 Let us consider axioms:

ax1: ∀x q(x) ax2: ∀x (q(x) ⇒ r(x)) ax3: ∀x (p(x) ∧ q(x) ∧ r(x) ⇒ s(x)
) and a conjecture:

∀x (p(x) ⇒ s(x)). A proof of this theorem, obtained with inlining (and with the derived lemma ∀X r(X))) looks as follows.

Consider an arbitrary a such that: p(a). It should be proved that s(a).

1. s(a) (by MP, from p(a), q(a), r(a) using axiom ax3; instantiation: X → a)

Proved by assumption! (by QEDas)

Since simple axioms cannot be applied on their own within MP steps (all applications of simple axioms are kept implicit within applications of other axioms), it is necessary to derive all their consequences in the form of simple axioms and add them to the set of the original axioms (we call this process "saturation").

This technique contributes to the generation of readable proofs because simple axioms are often omitted in natural language proofs. For example, in geometry (which is our main source of applications), the following axioms, where Col is a predicate to designate colinearity, are simple:

∀ABC (Col(A, B, C) ⇒ Col(B, A, C)) ∀AB Col(A, A, B) ∀A A = A
A mathematician would hardly feel the need to explicitly state that two identical points are collinear with a third one, or that a point is equal to itself, even if these facts are needed for application of some theorems in some special cases. Readability of generated proofs is further discussed in Section 6.3. Fortunately, keeping such proof steps implicit also improves the efficiency of the prover.

Memoization. Memoization is a technique for speeding-up computations by storing results of certain function calls and returning the result when the same inputs occur again. In our context, instead of concrete values about proof steps we have only symbolic values. But something like memoization can still be applied. Some concrete conditions, for instance "proof steps 3 and 7 are on the same proof branch" may occur in several constraints. For such conditions, we introduce new variables, link the variable to the condition by a constraint, and in other constraints use the variable instead of the full condition. This leads to more concise constraints and can facilitate the solving process 11 .

Implementation

We implemented the above approach as a prover called Larus, 12 a C++ application, with a support of several external tools. 13 Although our implementation is fully functional, it is not fully optimised and should still be considered a prototype implementation, developed along the way of exploring the new automated proving approach. The approach is implemented in several variants, in a form of several proving engines (they have been implemented alongside one proving engine based on using forward reasoning and the data structures available via the STL (Standard Template Library) C++ library ). We have implemented support for encoding proofs in SAT (via the constraint solving system URSA) and in several SMT theories. The solving phase uses SAT and SMT solvers. We implemented support for filtering by external provers such as Vampire [START_REF] Kovács | First-Order Theorem Proving and Vampire[END_REF] which eliminates unnecessary axioms (explained in more details in Section 4.1). We also implemented a simplification procedure that eliminates redundant proofs steps (from proofs that are not shortest possible). The implementation consists of around 8000 lines of code (around 7000 lines without the STL-based engine).

The overall proving pipeline in this implementation looks as follows:

1. read the axioms and the conjecture given in the TPTP/fof format; 2. use filtering; 3. transform the axioms and the conjecture from CL to CL2 form; 4. use filtering; 5. encode a proof of the conjecture -on the basis of the given axioms and the conjecture, generate constraints in terms of dedicated variables and possibly (for some SMT-based engines) in terms of interpreted (e.g., +) and uninterpreted functions (e.g., Nesting ); 6. invoke a suitable solver and retrieve the model found (assuming it exists); 7. read the values of relevant variables (some are redundant) and reconstruct the CL2 proof encoded as a sequence of natural numbers; 8. read the CL2 proof encoded as a sequence of natural numbers, decode it and construct a proof in terms of internal data-structures; 9. simplify the proof (delete redundant proof steps); 10. transform the proof from CL2 to CL form; 11. transform the proof in terms of internal data-structures into one of supported export formats, such as Coq proofs or natural language L A T E X proofs. We skip technical steps and discuss only some key design and implementation details.

Pre-processing and Filtering

Sledgehammer is a tool (nowadays -rather a methodology) that enables invoking automated theorem provers from the interactive theorem prover Isabelle [START_REF] Paulson | Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers[END_REF]. If external provers prove the given goal, they provide information that are used for reconstruction of a proof object within the interactive theorem prover. One of the tasks that external provers ( e.g., Vampire) do is filtering relevant axioms/clauses given. The user can provide hundreds of available axioms/clauses and filtering can, using different techniques, discard many of them, before an attempt to prove the theorem. We use a similar approach for pre-processing the axiom set before trying to prove the conjecture by our prover.

For filtering we use the FOL theorem prover Vampire [START_REF] Kovács | First-Order Theorem Proving and Vampire[END_REF]. In the first filtering phase, the given conjecture with all given axioms (in CL form) is sent to the external prover (Vampire). If it proves the conjecture, the list of used axioms is extracted and forwarded to further proving steps (otherwise, the set of all axioms is used); The second filtering phase, after the axioms are transformed into CL2 form, goes through several stages:

the given conjecture with all the axioms in CL2 form is sent to the external prover. If it proves the conjecture, the list of used axioms is extracted and forwarded to further proving steps (otherwise, the set of all axioms is used); -the equality predicate symbol is replaced by a dedicated predicate symbol, and the axioms and the conjecture are sent to the external prover. The point is in avoiding using full native support for equality (in both the external and the presented prover). If the external prover proves the conjecture, it returns only instances of equality axioms that are really needed and only them will be used in the next proving steps. Otherwise, if the external prover fails, all instances of equality axioms will be used. -the negated predicate symbols are replaced by dedicated predicate symbols, and the axioms, along with the axioms

∀ x(R( x) ∧ R( x) ⇒ ⊥), ∀ x(R( x) ∨ R( x)),
for each predicate symbol R, and the conjecture are sent to the external prover. The point is in avoiding using the full native support for negation (in both the external and the presented prover). If the external prover proves the conjecture, it returns only the above axioms that are really needed. Otherwise, if the external prover fails, all of them will be used. Each filtering stage is optional and the proving procedure may go without them. Note that, if the filtering is used, it is not guaranteed anymore that the obtained shortest proofs are indeed the shortest over the initial set of axioms (since the external prover may have reached a proof based on some other axioms).

Apart from the above filtering based on an external prover, we have also implemented filtering based on reachability. We say that a predicate symbols is reachable if it occurs in the premises of the conjecture, or can be reached by applications of axioms in which all premises are over reachable predicate symbols. An axiom with a premise that is not over a reachable predicate symbols can be eliminated.

Implementation of the Proof Encoding

The notion of CL2 proof represented as a sequence of natural numbers is common for all the implemented constraint-based proving engines. Given some axioms and the conjecture, constraints describing a proof can be expressed in several ways. We support the following:

the constraints can be expressed in a high-level representation language offered by our constraint system URSA; -the constraints can be expressed in a low-level representation language of SMTlib.

Substantially, the constraints are the same but the URSA-based approach leads to a self-contained, concise proof specification (that includes representations of the axioms and the conjecture). For instance, constraints saying that a proof step is FirstCase step are expressed in the following way (the URSA code is generated by our prover):

14 bFirstCaseStep = (nAxiomApplied[nProofStep] == nFirstCase) && nProofStep>0 && bCases[nProofStep-1] && !bCases[nProofStep] && (nNesting[nProofStep-1] <= nMaxNesting) && (nNesting[nProofStep] == (nNesting[nProofStep-1]<<1)) && (nP[nProofStep][0]==nP[nProofStep-1][0]); for (nInd = 0; nInd < nMaxArg; nInd++) bFirstCaseStep &&= (nA[nProofStep][nInd]==nA[nProofStep-1][nInd]);
In the URSA-based approach, representations of different theorems differ only in the encoding of axioms and the conjecture itself, while the encoding of the notion of proof is common. It consists of only around 300 lines of URSA code. Therefore, development of an automated theorem prover for CL is reduced to a relatively small human effort of making this 300-lines specification, plus encoding of specific axioms and goals. The difficulty in our work was, however, the road from the initial general idea to the fully functional system requiring a number of peripheral modules, and also exploring a number of variations of encodings and looking for one that leads to efficient solving by SAT provers. We have experimented with different variations, but we think there is still room for improvements. With the experience gained and the infrastructure developed, we believe that a support for another logic, contained in another few hundreds lines, would take significantly less time.

In the SMT-based approach, the specification of the notion of proof is spread through C++ code which is later translated to SMT constraints. This specification is less readable than URSA specification, but leads to more efficient theorem proving. 14 There are some small differences between the description of proof step FirstCase (Section 3.7) and the implementation. It can be shown that the condition StepKind (s -1) = MP , is redundant (since the previous step has to be branching), so it was omitted in the implementation. The constraint nNesting[nProofStep-1] <= nMaxNesting is not given in the description of proof step FirstCase . Indeed, this constraint is optional. Limiting the maximal nesting simplifies the problem and cuts-off some parts of the search space. If there are no branching axioms, by using this constraint it can be easily stated that there are no nesting at all. URSA constraints expressed in the above way are processed by URSA, bitblasted into SAT instance and sent to a SAT solver. On the other hand, in SMTbased engines, the constraints are right away expressed in terms of the low-level SMT representation. The following C++ code generates constraints saying that a proof step is a FirstCase step in SMT-lib form (for the case nProofStep > 0, sbFirstCaseStep is trivially false otherwise): sbFirstCaseStep = "(and " + appeq(app("nAxiomApplied", nProofStep), eFirstCase) app("bCases", nProofStep-1) + "(not " + app("bCases", nProofStep) + ") " + smt_less(app("nNesting",nProofStep-1), mParams.max_nesting_depth+1) + appeq(app("nNesting", nProofStep), smt_prod(app("nNesting", nProofStep-1),2)) + appeq(app("nP", nProofStep, 0), app("nP", nProofStep-1, 0)); for (unsigned nInd = 0; nInd < mnMaxArity; nInd++)

sbFirstCaseStep += appeq(app("nArg", nProofStep, nInd), app("nArg", nProofStep-1, nInd)); sbFirstCaseStep += ")";

If the equality symbol occurs in the conjecture, the equality axioms are added to the axiom set. If inlining is to be used and if there is equality in the axioms, then, in addition to simple axioms, equality substitution axioms are also inlined.

Arithmetic constraints can be represented in linear arithmetic or in bitvector arithmetic. Constraints involving functions can be represented in terms of uninterpreted functions (such as Nesting ) or Ackermanization can be used. So, there are four SMT-based encodings: LIA (linear integer arithmetic), BV (bit-vector arithmetic), UFLIA (linear integer arithmetic with uninterpreted functions), UFBV (bit-vector arithmetic with uninterpreted functions).

A proof is encoded as a finite object: there is a maximal number of proof steps, a maximal number of premises of the axioms, a maximal nesting , a maximal number of new constants introduced in each step, etc. Zero-based counting (like in C/C++) of proof steps, atomic formulae within steps, etc. is used, for a more compact representation.

The maximal number of premises of the axioms and maximal arity in predicate symbols can be computed based on the axioms. Concerning the maximal number of proof steps, we preserve completeness by an iterative increase of this constant (as discussed in 3.9). For ensuring completeness, the same should be done for the maximal nesting.

The logical constants ⊥ and are accepted as possible atoms in CL formulae, and they need a special treatment, since their truth values are fixed. Hence, such treatment augments the description of MP steps and constraints describing the goal.

In order to make the encoding simpler, there is the same number of slots for arguments in constraints for all atomic formulae (that number is determined based on the theory signature such that it can accommodate arguments for all predicate symbols). That brings some constraints/memory overhead, but it also enables simpler encoding. In the same spirit, new constants are represented by new natural numbers: w • s + i, i = 0, . . . , w -1, where s is the number of the proof step, and w is the maximal number of existential quantifiers in the axioms.

The encoding depends on the number of binary digits in URSA, BV, UFBVbased approaches. The default value is 12.

As a kind of optimisation, the information of StepKind and AxiomApplied for one proof step are stored in one number representing that step: the possible values are firstly possible step kinds (except MP ), and then axioms (with the ordinal numbers starting from the last possible step kind). Based on the value in the model, it is then trivial to decode StepKind and, if relevant -AxiomApplied .

In all proving engines, two proof steps s and s , while s precedes s are on the same proof branch if, considering the binary representation of these numbers, some prefix of the nesting of s equals the nesting of s : PREFIX(Nesting (s)) = Nesting (s ). This condition can be represented in all encodings by listing several possible cases (i.e., cases for all possible prefixes).

We find the URSA-based approach more flexible and better suited for debugging. However, the SMT-based approach with BV gives a better performance and most of the performance results given below are obtained using this encoding.

Generated SAT and SMT formulae are usually large, even for simple problems. For instance, for the conjecture from Example 10, the search for a proof of length 14 (via URSA) generates a SAT formula with 40817 variables and 249212 clauses. The SMT file with the corresponding problem description for the theory of bitvectors has 558 variables and the size of 815 Kb.

Implementation of Proof Decoding and Export

Generated constraints are passed to underlying solvers: clasp [START_REF] Gebser | clasp : A Conflict-Driven Answer Set Solver[END_REF] for URSA-based engine, and z3 [START_REF] Mendonça De Moura | Z3: An Efficient SMT Solver[END_REF] for SMT-based engines (although other solvers can be used as well). If the set of constraints is satisfiable, the solver returns a model. The values of relevant variables are read and a proof outline is generated (an example is shown in Section 3.5). This outline is read and a proof in internal (C++) representation is constructed. is decoded as follows:

the nesting equals 1; -the axioms are numbered from 13, hence, the step kind is MP and the axiom applied is the 0th axiom (i.e., ax1), -the derived formula is branching; -in the derived formula, in the first disjunct, the dominant predicate symbol is the 4th predicate symbol (i.e. r), and in the second disjunct, the dominant predicate symbol is the 6th symbol (i.e. q). In both, the argument is the 0th constant (i.e. a).

The two branches in the proof have nesting 2 and 3 (10 and 11 in binary representation) and, according to the given criterion, they are not on a same proof branch, as expected.

The internal proof representation is simply exported to a needed output format. Currently, there is support for the Coq format, and for an informal, natural language proof format (an example is shown in Section 3.5)

For Coq proofs, we preserve the forward chaining and declarative style of the proof by using the standard assert tactic of Coq and some user defined tactics to keep the small granularity in the proofs as in the natural language output. For example, we introduce a tactic by cases on, allowing to perform case distinction on previously proved logical disjunctions by referring to the actual statement rather than the name of the hypothesis. Contrary to other CL provers (such as the one of Bezem [START_REF] Bezem | Automating Coherent Logic[END_REF]), the export to Coq is expressed at the tactic level rather than as a lambda term. The export as a sequence of Coq tactics has several advantages:

-It allows the use of Coq's automation to both reduce the size of the proof and ease the checking of the proof by rebuilding some pieces of information at the checking time.

-It preserves the readability and maintainability of the proof.

The tactic conclude solves the remaining goal if it is a previously proven statement, or a disjunction containing a previously proven statement instantiating the potential existential variables. Conjunctions are split by the tactics implicitly at each proof step. As an example, we provide the Coq proof for Example 1:

Require Import src.general_tactics. Require Import Classical. Section Sec.

Parameter MyT : Type. Parameter p : MyT -> Prop. Parameter r : MyT -> Prop. Parameter q : MyT -> Prop.

Hypothesis ax1 : forall X : MyT, p X -> r X \/ q X. Hypothesis ax2 : forall X : MyT, q X -> False.

Theorem example_with_false : forall X : MyT, p X -> r X. Proof. intros a. intros. assert (r a \/ q a) by applying (ax1 a). by cases on ( ( r a ) \/ ( q a ) ).

-{ conclude. } -{ assert (False) by applying (ax2 a). contradict. } Qed.

End Sec.

For support of simple lemma inlining, we first prove the lemma obtained by saturation in sequence using automation. Those lemmas are put in a so-called "hint base". The lemmas are then used implicitly in the main proof. For each proof step which requires a given premise, the premise can be obtained by assumption or by using the inlined lemmas.

Configuring

The provers can be configured using several parameters, including the following ones: an input format, an initial (maximal) proof length, a final (maximal) proof length, a maximal nesting, a flag whether a shortest proof should be found, a flag whether proof simplification is to be used, a flag whether axiom inlining is to be used, a flag whether excluded middle axioms (for existing predicates) are to be used, a flag whether negation elimination axioms (for existing predicates) are to be used, a flag whether filtering is to be used, a flad saying if an interactive theorem prover should verify generated proofs, and a time limit.

Performances and Evaluation

For evaluation, we cannot use the standard TPTP benchmarks because the benchmarks are not in coherent logic form. Despite the fact that these benchmarks could be translated to CL by some procedure [START_REF] Dyckhoff | Geometrization of first-order logic[END_REF], we want to test our implementation on goals which are naturally in coherent form. We ran our implementation on several corpora listed below.

We compared performance of our prover to performance of several state-ofthe-art, award-wining FOL provers (Vampire, E, Iprover), provers with a small implementation (leanCoP, nanoCoP), one prover based on coherent logic (Geo), a prover generating Coq proofs (Zenon), some Coq tactics (first-order and Coq Hammer) and a prover using a technique related to ours (ChewTPTP). We did not test other CL based provers because they do not accept TPTP syntax (but the prover we tested (Geo) was the most efficient prover among several CL provers in one previous study [START_REF] Bjarne Holen | Efficient Rule-Matching for Automated Coherent Logic[END_REF]). The list of provers/versions is the following:

-Vampire 15 4.4 using CASC mode [START_REF] Kovács | First-Order Theorem Proving and Vampire[END_REF], a superposition-based theorem prover; -E 16 2.2 in auto mode, a superposition-based theorem prover; -Iprover 17 3.1e [START_REF] Korovin | iProver -An Instantiation-Based Theorem Prover for First-Order Logic (System Description)[END_REF], an instantiation-based theorem prover for first-order logic; -leanCoP 18 2.1 [START_REF] Otten | leanCoP: lean connection-based theorem proving[END_REF], a prover based on the connection (tableau) calculus; -nanoCoP 19 1.1 [START_REF] Otten | nanoCoP: Natural Non-clausal Theorem Proving[END_REF], a prover based on the non-clausal connection calculus for classical logic; -Geo 20 2007f, a prover based on geometric resolution; -ChewTPTP 21 1.0.0 [START_REF] Bongio | Encoding First Order Proofs in SMT[END_REF], which proves rigid first-order theorems by encoding the existence of a first-order connection tableau in SAT; -Zenon 22 0.8.4 [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF], a prover based on the tableau method and capable of producing Coq proofs; -Standard first-order tactic of Coq, a reflexive implementation of a first-order prover [START_REF] Contejean | Reflecting Proofs in First-Order Logic with Equality[END_REF]; -Coq Hammer Tactics 23 v1.3 [START_REF] Czajka | Practical Proof Search for Coq by Type Inhabitation[END_REF].

-Isabelle Hammer in TPTP mode without proof reconstruction 24 [START_REF] Paulson | Isabelle: A Generic Theorem Prover[END_REF].

For converting problems from TPTP to Coq, we used tptp2coq 25 . For converting problems from TPTP/fof to the clausal form required by Geo and ChewTPTP, we used Vampire. The evaluation was performed on a PC working under Linux, with Intel(R) Core(TM) i5 CPU 750 @ 2.67GHz, 20GiB SDRAM.

Elements corpus

This corpus is the set of 234 lemmas and propositions coming from the formalisation of the first book of Euclid's Elements [START_REF] Beeson | Proof-checking Euclid[END_REF]. The proofs of these theorems, constructed by humans, have already been checked by both Coq and HOL-Light interactive provers. All lemmas and propositions are naturally expressed in CL or can be very simply modified to belong to this fragment. This is a rich, real-world corpus, with instances ranging from trivial to very complex. But we agree with Avigad that this kind of benchmarks are not fully realistic for testing effective usability of automation in an ITP context in practice [START_REF] Avigad | Automated reasoning for the working mathematician[END_REF]. For example, within 100s, Vampire can prove 25 and Larus can prove 13 of the 73 statements corresponding to the propositions from the first book of Euclid's Elements, but the reader should not interpret these results as "ATP can solve automatically around a third of Euclid's propositions." Namely, the corpus contains all lemmas and axioms that are necessary for proving Euclid's propositions, and those have been discovered in the first place only by building the proofs manually using a proof assistant.

The formal proofs constructed manually allow us to compare them to the proofs generated automatically by our prover, but also to evaluate the difficulty of the theorems by measuring the size of the handcrafted formal proofs. Comparison between different prover configurations. On this corpus, we compared the performance of different configurations of the Larus prover. For the base configuration, we used the SMT-BV based engine and the solver z3, with an initial proof size of size 8, using lemma inlining, and without filtering. We also used (all without filtering):

Larusstl: based on a pure forward chaining saturation algorithm (using simple STL C++ structures); Laruslia: based on the SMT-LIA based encoding and the solver z3; Larusursa: based on the encoding of the problem into SAT, using the system URSA and the underlying SAT solver clasp; Larus-i: based on the SMT-BV encoding and the solver z3, but without lemma inlining.

The experimental results, shown in Figure 1, show that the best configuration (among considered ones) is the base configuration. The simple forward-chaining engine showed a typical behaviour: what can be proved is what can be proved in a short time, and then providing more time does not improve that much the results. In further experiments and comparisons to other provers, we consider only the base, SMT-BV-based configuration of Larus (Larusbase), with fixed, suitable parameters for specific corpora. Comparison with other provers. Comparing to other provers (Figure 2), Larus' performance is similar to some provers that have small implementations, but are still very efficient, such as Leancop. State-of-the-art general FOL provers give a significantly higher success rate. Overall, the best performance was by Vampire. Larus outperforms other provers producing Coq proofs such as Zenon, or Coq tactics.

We have verified experimentally that the size of the formal proof built interactively is a good measure of the difficulty of the theorem for ATP, as shown in Figure 3. For all the provers, the percentage of theorem proved against the size of the human-crafted proofs is more-or-less strictly monotonically decreasing. All the provers except ChewTPTP and Zenon can prove almost 100% of theorems with short proofs. Larus meets this patterns too for short proofs, but Larus cannot find large proofs with more than 50 steps. However, as Larus proceeds by increasing progressively the size of potential proof, along the way, Larus also confirms the absence of proofs of shorter sizes. On all our benchmarks, Larus' results are better than those of ChewTPTP, which is a similar approach based on SMT solvers, and this shows that encoding within CL gives better results. The results for Isabelle have the shape with steps because Isabelle first tries some tactics that cannot solve the goals, and later calls state-of-the-art provers such as Vampire that can solve some of these goals instantly.

Coherent corpus

This corpus is the set of 64 benchmarks used in previous research26 about automatic theorem proving in CL [START_REF] Bjarne Holen | Efficient Rule-Matching for Automated Coherent Logic[END_REF]. These benchmarks contain both simple and difficult examples. Some originate from the formalisation of Hessenberg's theorem [START_REF] Bezem | On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic[END_REF].

Some theorems, if considered in the CL setting, require proofs with no less than 100 or 200 steps, which was too difficult for our prover (for some of these, there is a small search space for the forward chaining approach, hence they can be easily proved by the engine Larusstl). On these benchmarks, the Geo prover competes well with state-of-the-art provers (Figure 4). Again on these benchmarks, Larus cannot compete with state-of-the-art FOL provers, but outperforms ChewTPTP, Zenon and the Coq tactics.

col-trans corpus

This corpus is a set of 1361 sub-goals used in the formalization of geometry concerning some properties about pseudo transitivity of collinearity which are easy to solve using an ad-hoc procedure [START_REF] Boutry | A reflexive tactic for automated generation of proofs of incidence to an affine variety[END_REF], but are more challenging for some general purpose ATPs. This corpus originates from a concrete application: we would like to export the large Coq library of geometry proofs GeoCoq27 to Logipedia [START_REF] Dowek | Logipedia: a multi-system encyclopedia of formal proofs[END_REF]. However, in the Coq formalisation, these sub-goals are currently solved by a reflexive Coq tactic (called ColR), the result of which cannot currently be checked by Dedukti. We do not include the ColR tactic in the benchmarks because it is not a general purpose prover. This corpus is a challenge for hammers such as Coq Hammers, because the set of axioms needed is already known and is small. Hence, calling a state-of-the-art prover does not help to reduce the difficulty of the proof search within the proof assistant. The results for Isabelle do not include proof reconstruction. Isabelle hammer is running several state-of-the-art provers sequentially: if the first tactics fails, then Vampire is called and can solve the goal. For this corpus, Larus is used with options: no case splits, start by looking for a proof of at most 8 steps, and check the generated proof using Coq . 28

Crafted corpus

We consider the following schema of conjectures (parametrised by n):

ax1: dom(a We generated instances of the above schema for n equal 1 to 100. This crafted set serves to explore behaviour of our prover in situations where there is a very short proof, but it is hard to be found by procedures based on instantiations and model finding/evolution. Indeed, Larus performed very well on this corpus 29 , and outperformed by far Iprover and Geo which had poor performance. Larus' performance was also much better then that of ChewTPTP. On the other hand, all provers based on the resolution method or some related methods had excellent results. These results suggest that automated theorem proving in CL (like in other logics) can benefit from having available different proving techniques (as discussed in Section 8.3).

Summary of Experimental Results

On the considered corpora, the provers Vampire and Eprover showed best performance and Larus' performance was generally worse than performance of these state-of-the-art FOL provers. On most corpora, Larus outperformed provers that generate verifiable proofs such as Zenon, and also the prover ChewTPTP, the prover that is most closely related to Larus among the considered provers in terms of the proving approach. Concerning the main target domain, the most closely related prover is Geo, and it outperformed Larus on most of the corpora, but not on the crafted corpus. On this corpus Larus also significantly outperformed Iprover.

Overall, the experimental results suggest that Larus shows reasonable performance and that it can be practically usable in some situations, primarily when a verifiable and/or readable proof is needed.

Features and Perspectives

The presented approach provides a suitable basis for various applications and upgrades. In this section, we discuss some of them, like generation of shortest, readable, or machine verifiable proofs.

Short Proofs, Shortest Proofs, All Proofs

Shorter proofs are often preferred: for their beauty or for more practical reasons such as saving space in a printed article or in a computer formalisation. The quests for short, simple or simplest proofs are among the oldest quests in mathematics, as argued by Wos [START_REF] Wos | Automating the Search for Elegant Proofs[END_REF]:

The search for elegant proofs has continuously played a key role in mathematics and in logic. Such a search can lead to the discovery of new, important relationships, and it can also lead to the formulation of significant concepts. In addition to the aesthetic aspects of elegance of concern to mathematics and logic, practical aspects also exist, easily illustrated when the focus is on proof length. Indeed, the methodology here may also serve well in the context of constructing more efficient circuits synthesizing more effective algorithms, and the like.

The challenge of finding simplest proofs was even an item (a lost one!) on the famed Hilbert's list of the most significant mathematical problems [START_REF] Thiele | Hilbert's Twenty-Fourth Problem[END_REF]:

The twenty-fourth problem in my Paris lecture was to be: Criteria of simplicity, or proof of the greatest simplicity of certain proofs.

There are several ways to define what the simplest proof of a theorem is, but the most common one is based on proof length -the number of inference steps applied [START_REF] Kinyon | Proof simplification and automated theorem proving[END_REF]. There are just a few concrete results for practical finding of short or shortest proofs automatically, although there are several possible approaches for this task, usually based on some form of exhaustive search and resolution method [START_REF] Kinyon | Proof simplification and automated theorem proving[END_REF][START_REF] Veroff | Finding Shortest Proofs: An Application of Linked Inference Rules[END_REF][START_REF] Wos | Automating the Search for Elegant Proofs[END_REF]. Shortest proofs could be obtained also using simple breadthfirst search. There are also theoretical considerations on computability of functions that compute shortest proofs.

The approach presented in this paper provides a general method for finding shortest proofs in CL, but could be used for other underlying logics. We do not claim that it can outperform other possible approaches and a deeper study in this direction is needed (for instance, the examples from literature involve function symbols, which would require reformulation into CL). Still, we addressed this problem to some extent and we analysed the set of proofs crafted by a human, using some automation and then formalized within Coq [START_REF] Beeson | Proof-checking Euclid[END_REF]. Our prover found several proofs shorter than the originals and with unsubstantial differences, but also some substantially different proofs (see Section 6.3).

In the context of proof length and short proofs, it is interesting to address monotonicity for proof lengths. We can formulate monotonicity as follows: for a given conjecture, if there is a proof of size L, then for each L , such that L > L, there is a proof of size L . If monotonicity holds, then a simple binary search guarantees finding shortest proofs. However, monotonicity does not hold for our CL proofs. This is illustrated by the following example. However, there is no proof of length 8. Indeed, one cannot apply anything more with respect to the given proof. One could apply excluded middle, but then more steps will be needed.

All proofs. In some contexts it can be interesting to have all proofs of length less than n for a given conjecture. In the proposed approach, it is trivial to obtain all such proofs (or all proofs that meet some criterion) -it is just that all models of the generated constraints should be found. Having available all proofs of a theorem (within some logical framework) can be useful, for instance, in the context of education: "intelligent tutor systems" for mathematics education should be able to know all possible ways to solve a problem so they can help the students by anticipating their next steps (one such system, developed by Font et. al, based on a form of exhaustive search and implemented in Prolog, generates all proofs of geometry theorems using a custom set of axioms [START_REF] Font | Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context[END_REF]).

In some cases, it can be also interesting just to count the number of proofs of length ≤ MaxL (for instance, in the educational context, the number of proofs could measure appropriateness or difficulty of an exercise). If SAT is the target problem, there are efficient techniques for counting all models [START_REF] Lagniez | On Preprocessing Techniques and Their Impact on Propositional Model Counting[END_REF].

Proof Hints

The hints within the presented approach are its unique feature: many other provers can accepts hints or axioms that may be used (possibly with a higher priority), while, on the other hand, a hint for our prover means that it must be used. This feature reminds of GPS navigation: with GPS navigation, the user can ask for a road from a point A to a point B, but he/she can also ask for a road that goes via certain waypoints. It is similar with proving: other provers can be asked for a proof for some goal from some given premises, but (only) the presented approach can be also given some waypoints, some concrete steps that the proof must contain. Many kinds of waypoints can be given as simple additional constraints (over the set of already introduced unknowns). These waypoints may be useful, for instance, in full reconstruction of proofs given only an outline (like proofs in textbooks). This could be a step towards a target discussed by Gowers and Hales [START_REF] Hales | An argument for controlled natural languages in mathematics[END_REF]:

One dream was to develop an automated assistant that would function at the level of a helpful graduate student. The senior mathematician would suggest the main lines of the proof, and the automated grad student would fill in the details.

A waypoint step that is provided can, of course, be totally irrelevant and superficial in the generated proof. However, if it is relevant and if, in addition, one asks for a shortest such proof, the proof is likely to heavily use the given steps/waypoints. Note that this approach is much more general than just splitting the problem into sub-problems: find a road from A to B and then a road from B to C. In our context, the waypoints do not have to be ordered (one can ask for a proof using X and Y in no particular order), the waypoints can be vague, imposed only by partial constraints (e.g., "find a road going through some city" or "find a road going through some region", "find a road of length between d 1 and d 2 " or, in our terms: "find a proof that uses some predicate symbol", or "find a proof using some lemma", without the way it is instantiated, etc). In a similar spirit, some axioms or the goal can be given imprecisely and the system could reconstruct them, along with a proof. Of course, one has to be careful and avoid trivial reconstructions (like an inconsistent set of axioms).

Our hints are different from "proof sketches" used in resolution based provers [START_REF] Kinyon | Proof simplification and automated theorem proving[END_REF][START_REF] Veroff | Finding Shortest Proofs: An Application of Linked Inference Rules[END_REF], where "hints" are "important clauses, notable milestones toward a proof, because they already occurred in another proof of a stronger theory" and they provide patterns for giving higher priority to some sets of clauses. Using our analogy, proof hints in resolution provers are cities, such that if the algorithm happen to find a route through one of such cities, it will give a preference to this city in further search. Our hints could be a first step toward implementing a proof assistant allowing "proof sketches" in the sense of Wiedijk, i.e., partial information about the proof looking like an informal proof and whose gaps could be filled by the use of automation [START_REF] Wiedijk | Formal proof sketches[END_REF].

We have implemented support for the hints (for the URSA-based proving engine only). The implementation should be considered experimental. We slightly extended the language TPTP/fof to allow the specification of proof hints using a simple but still quite expressible semantics. Some features of this support and some kinds of hints (not all) are illustrated in the next example.

Example 9 Consider the following simple conjecture given in the TPTP/fof format.

fof(ax1, axiom, (! [A,B] : (p(A,B) => r(B,A)))). fof(ax2, axiom, (! [A,B] : (p(A,B) => q(B,A)))). fof(ax3, axiom, (! [A,B] : (r(A,B) => r(B,A)))). fof(ax4, axiom, (! [A,B] : (r(A,B) => p(B,A)))). fof(ax5, axiom, (! [A,B] : (q(A,B) => q(B,A)))). fof(ax6, axiom, (! [A,B] : (q(A,B) => p(B,A)))). fof(ch, conjecture,(! [A,B] : (p(A,B) => p(B,A)))).

fof(hintname0, hint, r(?,?), _ , _).

One hint is given above as an additional, last line that brings the above specification out of the TPTP/fof format . In addition to the first two slots (in the style of the TPTP/fof format), there are three more slots: the first one provides a pattern for the atom that should appear in the proof, the second one specifies the ordinal number of the proof step constrained, and the third one provides a pattern for the (instantiated) axiom used. Each of them may be non-specified or partly nonspecified. For instance, fof(hintname0, hint, r(?,?), _, _) imposes that a fact r(?,?) will be present in some step of the proof, while fof(hintname0, hint, q(2,1), 5, _) imposes that a fact q(2,1) will be present in the step 5 of the proof and the arguments will be the second and the first constant introduced. As another instance, fof(hintname0, hint, _, 3, ax2(A,A)) imposes that the axiom ax2 must be used in the step 3, in such a way that the first and the second universal variable are instantiated by the same constant.

The above conjecture can be proved either by using the predicate symbol r (and the axioms ax1, ax3, ax4), or the predicate symbol q (and the axioms ax2, ax5, ax6). We will illustrate how different hints can bring us to different proofs. The given hint imposes using the predicate symbol r while it does not impose any condition on its argument, or about the proof step where r is to be used. The generated shortest possible proof (without inlining) is as follows:

Consider arbitrary a, b such that: p(a, b). It should be proved that p(b, a). If, for instance, the following hint was given instead: fof(hintname0, hint, _, _, ax2(?,?)).

it imposes using the axiom ax2, and the generated shortest possible proof is as follows:

Consider arbitrary a, b such that: p(a, b). It should be proved that p(b, a).

1. q(b, a) (by MP, from p(a, b) using axiom ax2; instantiation: A → a, B → b) 2. q(a, b) (by MP, from q(b, a) using axiom ax5; instantiation: A → b, B → a) 3. p(b, a) (by MP, from q(a, b) using axiom ax6; instantiation: A → a, B → b) 4. Proved by assumption! (by QEDas) Finally, if the following hints were given: fof(hintname0, hint, r(?,?), 1, _). fof(hintname1, hint, q(?,?), 3, _). they impose using a fact r(?,?) in the step 1, and a fact q(?,?) in the step 3 of the proof (the assumption is the step 0). The generated shortest possible proof is as follows:

Consider arbitrary a, b such that: p(a, b). It should be proved that p(b, a).

1. r(b, a) (by MP, from p(a, b) using axiom ax1; instantiation: A → a, B → b) 2. q(b, a) (by MP, from p(a, b) using axiom ax2; instantiation: A → a, B → b) 3. q(a, b) (by MP, from q(b, a) using axiom ax5; instantiation: A → b, B → a) 4. p(b, a) (by MP, from q(a, b) using axiom ax6; instantiation: A → a, B → b) 5. Proved by assumption! (by QEDas)

Obviously, in the latest proof, the step 1 is useless, but it is there since it was imposed by the hint. For this proof, the simplification procedure was turned off. If it was used, as normal, the first step would be eliminated as redundant.

Readable Proofs

There is a long history of rigorous proof systems that allow readable, natural proofs. Natural deduction, developed in 1920's, is one of the first and still most notable such systems [START_REF] Gentzen | Untersuchungen über das logische Schliessen, I, II[END_REF]. Gentzen said: "I wanted to set up a formalism that comes as close as possible to actual reasoning". One of the key issues in readability of proofs are intuitive basic inference steps. But there is more in readability in proofs written by humans -readability is also a global property of the proof text. For example, human-style proofs or comprehensible proofs may omit many details but keep a substantial insight about why the theorem is valid. Recent approaches and challenges for automatically creating human readable proofs in geometry have been surveyed by Jiang et. al. [START_REF] Jiang | A review and prospect of readable machine proofs for geometry theorems[END_REF] or by Nguyen [START_REF] Nguyen | Design an intelligent problem solver in solid geometry based on knowledge model about relations[END_REF].

Comprehensible proofs can be difficult to verify by a machine, but still can be understood by humans. Constructing but also verifying such proofs is an interesting research topic on its own (there is a recent overview of candidates for controlled natural languages for the communication of mathematics [START_REF] Hales | An argument for controlled natural languages in mathematics[END_REF]), but it is not in the focus of this work. Still, we address a closely related task: generating rigorous proofs expressed in a strict formalism of CL with granularity similar to the granularity of natural language proofs. The CL proof system combines several natural deduction rules into one rule, thanks to which CL proofs often tend to be simpler and more natural than natural deduction proofs. Therefore, CL can serve well as a vehicle for readable proofs, and CL proofs can also suitably serve as a basis for further post-processing so they can be made even more human-style. In addition, the notion of a CL proof may be slightly modified into this direction, as discussed further.

Proofs expressed within CL can still be hard to read because the reader may be overwhelmed by uninteresting details. For example, in a natural language proof in a research level publication, no mathematician would state explicitly that: a) "ABCD is a rectangle because ABCD is square" or b) "ABCD is a parallelogram because BCDA is a parallelogram", because such details would hide the important steps of the proofs. Keeping some inference steps implicit is hence crucial for the readability of the proofs. What should be implicit or not is difficult to say in general and depends on the context. For instance, at the primary school level, pupils may be encouraged or asked to state explicitly claims like a), but not claims like b). Having implicit proof steps but also mechanical proof checking of such proof steps, is useful. In geometry for example, there is a long history of incorrect proofs of Euclid's fifth postulate, that relied on an implicit assumption equivalent to the fifth postulate. For example, if one defines a parallelogram as a non-crossed quadrilateral such that two sides are parallel and of the same length, then the property b) stated above is equivalent to Euclid's fifth postulate (see [START_REF] Boutry | Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq[END_REF] for more details about these issues).

As an extension of our basic approach, we use a variant of CL proofs, where proof steps allow implicit application of "simple" lemmas as described in Section 3.11. We have chosen to inline lemmas with at most one premise, but in natural language proofs sometimes proof steps involving several premises are also implicit, for example in geometry the transitivity of parallelism will usually not be stated explicitly. For Proposition 5 of Book I of Euclid's Elements, inlining leads to a quite readable proof, very similar to Pappus' proof, given in the following example (see appendix A for a full comparison of the proof of this proposition as generated by several provers).

Example 10 Euclid Book I, Proposition 5: In isosceles triangles the angles at the base equal one another. Or, in formal terms:

∀ A, B, C (isosceles(A, B, C) ⇒ congA(A, B, C, A, C, B) )
Pappus' proof is as follows: 30 The two triangles BAC and CAB have two sides equal to two sides, namely side BA of the first triangle equals side CA of the second triangle, and side AC of the first triangle equal to side AB of the second, and the contained angles are equal, namely angle BAC of the first triangle equals angle CAB of the second, therefore, by proposition I.4, the corresponding parts of the two triangles are equal, in particular, the angle B in the first triangle equals the angle C of the second.

Proposition I.4, mentioned in the above proof, corresponds to the Side-Angle-Side theorem stating: if two triangles have two sides equal to two sides respectively, and have the angles contained by the equal sides equal, then they also have the base equal to the base, the triangle equals the triangle, and the remaining angles equal the remaining angles respectively.

The above, Pappus' proof assumes that the triangle is not degenerated, but the following (shortest) proof generated by Larus distinguishes the case of the degenerated triangle , showing that it is impossible (using implicitly a simple lemma that vertices of isosceles triangle are not colinear and the axiom nnncolNegElim:

∀X, Y, Z col(X, Y, Z) ∧ ¬col(X, Y, Z) ⇒ ⊥).
Larus' proof does not give details about the fact that angle BAC is congruent to angle CAB, because it is a lemma that is considered simple enough to be inlined. The premise stating that abc is isosceles appears twice at step 6 because it corresponds to the two triangles (BAC and CAB) that appear in proposition I.4 (Side-Angle-Side theorem, named here Note that the quantity of information which should be kept implicit is difficult to control, as illustrated on Euclid's Proposition 43 in the next example. The ratio between the size of a formal proof and size of the natural language proof, called the De Bruijn factor, is rarely below 1. With Larus, for this theorem, we get a surprising result: the (shortest) formal proof generated using inlined lemmas (if we omit the proofs of the inline lemmas) is shorter than both the original natural language proof and the original formal proof (30 steps). 32 The idea of the proof is depicted on Figure 8. The formal proof generated by Larus is just a two line proof, given here in the natural-language: Consider arbitrary a, b, c, d, e, f , g, h, i such that: pG(a, b, c, d), betS(a, h, d), betS(a, e, b), betS(d, f, c), betS(b, g, c), betS(a, i, c), pG(e, a, h, i), pG(g, i, f, c).

It should be proved that eF (i, g, b, e, d, f, i, h). (c,i,h,d,b,e,i,c) (by MP, from betS(a, i, c), betS(a, e, b), betS(a, h, d), betS(a, i, c), pG(e, a, h, i), pG(a, b, c, d) using axiom axiom cutoff1; instantiation:

eF

A → c, B → i, C → a, D → h, E → d, Ca → b, Cb → e, Cc → a, Cd → i, Ce → c)
2. eF (h, d, f, i, e, b, g, i) (by MP, from betS(d, f, c), betS(b, g, c), pG(g, i, f, c), eF (c, i, h, d, b, e, i, c) using axiom axiom cutoff2; instantiation:

A → h, B → d, C → f , D → c, E → i, Ca → e, Cb → b, Cc → g, Cd → c, Ce → i)

Proved by assumption! (by QEDas)

The axiom cutoff1 says that if we cut triangles of equal areas, with one end of the cut at a vertex and the other two on the adjacent sides, from triangles with equal areas, the resulting quadrilaterals have equal areas. The axiom cutoff2 says that if we cut triangles with equal areas off of quadrilaterals with equal areas, with one end of the cut at a vertex and the other on a non-adjacent side, the results are quadrilaterals with equal areas.

In this case, the mechanism that generates inline lemmas by saturation of simple axioms, has gone quite far, maybe too far, because it generated about 400 lemmas, and then most of the proof is implicit! It means that the proof of Proposition 43 is mainly a composition of lemmas with a single premise.

In the first step of the proof, the fact that the triangles AEI and AHI have equal areas is deduced implicitly from the fact that EAHI is a parallelogram using Euclid's Proposition 34 (which states that the diagonal of parallelogram divides it into two congruent triangles) and a lemma stating that congruent triangles have equal areas and many technical lemmas about preservation of equality of area by 31 pG(A, B, C, D) stands for "ABCD is a parallelogram", betS(A, B, C) stands for "B is between A and C", and eF (I, G, B, E, D, F, I, H) stands for "IGBE and DF IH are figures with equal areas". 32 https://github.com/GeoCoq/GeoCoq/blob/master/Elements/OriginalProofs/ proposition_43.v permutation of the points. Similarly it is implicitly proved that the triangles ABC and ADC have equal areas.

We can further modify the look of our computer generated proofs so they are more like human-created proofs. For example, we can replace case splits by reductio ad absurdum in some cases, we can replace predicate symbols and logical connectives by some natural language wording, generate nicer looking names, etc. We leave this for future work, as in this paper we focus on the granularity of the proofs steps and the structure of the proof.

Reconstruction of Proofs within ITP Systems

Integration of automatic theorem provers within interactive provers and exchange of proofs is crucial for development of interactive theorem proving but it poses several difficulties. The main ones come from differences between the underlying logical frameworks of the ITP and the ATPs systems (higher-order logics vs firstorder logic) and the absence of standards for representing proofs in both worlds. There are several lines of research trying to address these problems. The TSTP format allows to represent proofs as a list of steps, and the language does not specify what are the acceptable proof steps [START_REF] Sutcliffe | The TPTP World -Infrastructure for Automated Reasoning[END_REF]. The Logipedia project provides automatic transformations between different logical frameworks [START_REF] Dowek | Logipedia: a multi-system encyclopedia of formal proofs[END_REF]. Tools called "hammers" have been developed for Isabelle/HOL [START_REF] Blanchette | Hammering towards QED[END_REF][START_REF] Christian Blanchette | Automatic Proof and Disproof in Isabelle/HOL[END_REF][START_REF] Christian Blanchette | Extending Sledgehammer with SMT Solvers[END_REF][START_REF] Christian Blanchette | More SPASS with Isabelle[END_REF], HOL4 [START_REF] Urban | ATP and presentation service for Mizar formalizations[END_REF], Mizar [START_REF] Kaliszyk | HOL (y) Hammer: Online ATP service for HOL Light[END_REF] and Coq [START_REF] Czajka | Practical Proof Search for Coq by Type Inhabitation[END_REF][START_REF] Czajka | Hammer for Coq: Automation for Dependent Type Theory[END_REF]. In many hammer systems, the ATP is used only to find relevant lemmas/axioms and the actual proof argument by the ATP system is rarely used. Instead, an automatic theorem prover integrated in the ITP system is ran, using lemmas/axioms filtered out, for constructing an acceptable formal proof. Therefore, for examples where the list of relevant lemmas/axioms is already known, the hammer approach using state-of-the-art FOL provers will not provide any useful information and will not be more efficient than solely automatic tactics integrated inside ITPs. In some hammer systems, external solvers are used to produce certificates based on which the proof objects are constructed within the ITP.

If one wants to obtain a readable proof within an ITP system, then the difficulty of reconstructing a proof from an ATP argument is even higher, because state-ofthe-art ATPs usually rely on clausification, Skolemization and proof by refutation. Blanchette has proposed an algorithm to reconstruct a forward chaining Isar proof from the resolution proof [START_REF] Christian Blanchette | Semi-intelligible Isar Proofs from Machine-Generated Proofs[END_REF]. The approach presented here has the advantage of allowing the trivial generation of machine verifiable proofs which are fairly readable: they do not rely on clausification nor proof by refutation, they are in the forward reasoning style and the proof steps are higher-level than natural deduction proofs. With the support of proof hints as described in Section 6.2, by extracting automatically hints from formal or informal proofs, this approach could also serve as a base for translators from one proof language to another.

Classical vs. Intuitionistic Logic

While, for instance, in the resolution method, classical logic and reasoning are deeply built-in, in the presented approach and when using the prover, one can easily choose whether to use excluded middle or not (and, hence, choose between classical and intuitionistic setting), it is just a matter of adding axioms. Also, as said in Section 2, the additional ¬Intro rule could be supported. On the other hand, this feature (of flexible control of fundamental axioms) increases costs and influences efficiency of the presented approach.

Proof complexity

The central problems in proof complexity are: what is the size of the smallest proof of a theorem F in some logical system and how difficult is it to construct such a smallest proof [START_REF] Atserias | Automating Resolution is NP-Hard[END_REF][START_REF] Mertz | Short Proofs Are Hard to Find[END_REF]. These problems are relevant for the work presented in this paper, but not of a concrete, practical value for implementing the prover. Namely, answers to the given questions are typically given in terms of bounds too loose to be useful for limiting and guiding our proof-searching process.

Related Work

In the previous sections, we mentioned some related research, for instance, in the context of short or readable or machine verifiable proofs. In this section we discuss research and systems most closely related to the one presented, especially in terms of proof encoding and of using SAT/SMT in automated theorem proving.

Coherent Logic provers. There are several automated theorem provers for CL [START_REF] Bezem | Newman's Lemma -a Case Study in Proof Automation and Geometric Logic[END_REF][START_REF] Bezem | Automating Coherent Logic[END_REF][START_REF] Bezem | On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic[END_REF][START_REF] Janičić | EUCLID -the Geometry Theorem Prover[END_REF][START_REF] Stojanović | A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs[END_REF]. Some of them use advanced methods for efficient rule-matching [START_REF] Bjarne Holen | Efficient Rule-Matching for Automated Coherent Logic[END_REF] or back-jumping and lemma-learning inspired by CDCL SAT solving [START_REF] Nikolić | CDCL-Based Abstract State Transition System for Coherent Logic[END_REF][START_REF] De | Subsumption Algorithms for Three-Valued Geometric Resolution[END_REF][START_REF] De | Geometric Resolution: A Proof Procedure Based on Finite Model Search[END_REF]. They all use some form of forward chaining, in contrast to the prover presented here. Only some of them produce machine verifiable proofs [START_REF] Bezem | Automating Coherent Logic[END_REF] or both machine verifiable and human readable proofs [START_REF] Nikolić | CDCL-Based Abstract State Transition System for Coherent Logic[END_REF][START_REF] Stojanović | A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs[END_REF].

Automated provers using SAT/SMT solvers. There are approaches in which SAT and SMT are used in first-order theorem proving. For instance, in showing inconsistency of clause sets, Schultz uses saturation and SAT solving -ground facts are represented by propositional variables and there is a periodic check of propositional consistency [START_REF] Schulz | Light-weight integration of SAT solving into first-order reasoners-first experiments[END_REF]. In Vampire, the AVATAR architecture also tightly integrates SAT/SMT solvers [START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF].

These approaches are completely different from ours as SAT formulae are used for modelling the object level (formulae of underlying theory), while in ours, SAT/SMT formulae model the meta level, the level of proofs.

SAT solving is used also in higher-order theorem proving. For instance, there are complete theorem proving procedures, implemented in a prover Satallax, for higher-order logic based on a complete, cut-free, ground refutation calculus that delegates different tasks to a SAT solver [START_REF] Brown | Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems[END_REF]. Like in the case of first-order logic, SAT formulae do not model proofs, but again formulae, in contrast to our approach.

Proof encoding. The idea of encoding a proof by numbers dates back at least to Gödel's enumeration of proofs by which (in the context of his famous theorems) he demonstrated that deduction operations can be described in terms of numbers and arithmetical operations [START_REF] Smith | An Introduction to Gödel's Theorems[END_REF]. However, apart from such theoretical usage, there are hardly any practical applications of proof encoding in automated or interactive theorem proving . We are aware only of the following ones and they are the most closely related work.

There is a work on encoding propositional resolution proofs in propositional logic [START_REF] David | Local Search for Unsatisfiability[END_REF]. This is done trying to show that local search methods (suitable for solving satisfiable SAT instances) can be applied to unsatisfiable SAT instances. Our approach is also an alternative way of transforming unsatisfiability checking (using refutation) into satisfiability checking (i.e., checking existence of a proof).

Rigid tableau proofs (a rigid tableau is a tableau in which multiple instances of a clause appearing in the tableau are identical copies of the clause appearing in the given formula) can be encoded as a SAT problem, as in a system ChewTPTP-SAT [START_REF] Deshane | Encoding First Order Proofs in SAT[END_REF]. There are some problem instances that can be proved using this approach, and not by other provers, but the conclusion is that this approach is still not competitive to leading FOL provers. That work extends to encoding of the existence of a rigid first-order connection tableau to SMT (datatypes and arithmetic) [START_REF] Bongio | Encoding First Order Proofs in SMT[END_REF][START_REF] Ralph | Automated Theorem Proving Using SAT[END_REF]. It was shown that SMT-based encoding is more efficient than SAT-based encoding, but there is no experimental comparison to other kinds of provers. Machine verifiable or readable proofs are not considered. The prover ChewTPTP-SMT based on this approach was used for our experimental comparison given in Section 5.

Alrabbaa et.al. addressed the problem of finding small proofs in description logic (DL) [START_REF] Alrabbaa | Finding Small Proofs for Description Logic Entailments: Theory and Practice[END_REF]. They encode DL proofs as labelled, directed hypergraphs, where each hyper-edge corresponds to a single derivation step, and they study the complexity of the problem of finding the smallest DAG-shaped and tree shaped DL proofs.

Future Work

We are planning to implement export of proofs to Isabelle and other interactive theorem provers.

The first implementation of the presented approach shows proving performance below the state-of-the-art provers such as Vampire. We think there is a room for improvements of efficiency in the following directions:

improving the encoding used (e.g., by using some form of incremental encoding); -improving the solving process (e.g., by using some other SAT/SMT solvers, or by instructing SAT/SMT solvers to take into account some specifics of input instances); -improving the communication between the prover and the external solvers. Apart from the above (still rather vague directions), we consider several ways for improving the prover, discussed in the rest of this section.

Normalization of CL Proofs and Application to Automated Theorem Proving

Normalisation of proofs has been present for decades as one of central topics in proof theory. For instance, permutability of inference rules has been studied from a theoretical point of view since a long time, by Kleene in the 50's [START_REF] Cole | Permutability of inferences in Gentzen's calculi LK and LJ[END_REF] and more recently by Dyckhoff et. al. [START_REF] Dyckhoff | Permutability of proofs in intuitionistic sequent calculi[END_REF], Guenot [START_REF] Guenot | Concurrency and Permutability in the Sequent Calculus[END_REF], Lutovac and Harland [START_REF] Lutovac | A contribution to automated-oriented reasoning about permutability of sequent calculi rules[END_REF], etc. However, to our knowledge, it has been hardly used in automated theorem provers during the search process. Namely, the provers do not look for a proof, but for a formula and they usually introduce many superficial formulae along the way. During that process, it is not known which of them are really needed and how to use some normalisation criterion over them on the fly. In our approach, however, we can impose restrictions on a sought proof directly (no superficial facts) and we can also impose some normalisation criterion as an additional constraint. Actually, in the current version of the system, we already use some normalisation criteria: a case split can occur only at the end of a proof, the first case step occurs immediately after the disjunction has been derived, etc. By imposing restrictions on the form of a proof, some parts of the search space can be eliminated early which could facilitate the process. But, on the other hand, the number of possible models (i.e., proofs) will be smaller which could make search harder. We are planning to explore these ideas further and we hope that our approach could lead to new practical applications of normalisation results coming from proof theory.

Paralellisation

Let us assume one wants to prove a theorem for which a shortest proof has k steps, the number not known in advance. When searching for a proof of the theorem, one must provide a concrete, maximal proof length. If the chosen length is small, the chances are good for a quick response, but if it is lower than k, the proof will not be found (also, proving that there is no proof of some given length sometimes takes more time than finding a proof of a larger length). On the other hand, if the chosen length is big, it could be likely that there is a proof of smaller length, but the proving process can be slow and maybe over the given time limit. Therefore, it can be beneficial if different maximal proof lengths are considered in parallel. Some parts of the encoding can be shared, but the proving process can be completely independent and can be simply performed in parallel. We will work on this simple paralellisation and look for other potentially beneficial forms of paralellisation.

Using Other Kinds of Provers

We observed there are theorems that the presented approach cannot prove in some reasonably short time, while they can be proved by our simple forwardchaining based prover in a negligible time. The explanation is, we believe, that these theorems admit proofs in which in many steps one can proceed in just a very few ways -many steps are almost uniquely determined. For such theorems there are relatively long proofs (e.g., more than 200 proof steps), but substantially very easy for the forward-chaining approach. This observation leads to the following possible directions for future work:

-One can combine the presented approach with other kinds of provers, as they can be best performing on different sets of theorems. Combining different provers can be done in a well-developed portfolio approach [START_REF] Nikolić | Simple algorithm portfolio for SAT[END_REF][START_REF] Xu | SATzilla: Portfolio-based Algorithm Selection for SAT[END_REF]. An additional challenge (probably well-suited to machine learning) would be to detect which provers are better suited for which theorems. Actually, within a portfolio, one can use not only different provers, but also different configurations of Larus (given by its parameters). -One can use the forward-chaining approach along the proving process for shaping additional constraints that could help the prover based on constraint solving.

-One can try to help the SAT/SMT solvers in solving the constraint corresponding to a proof. Choosing decision variables is one of critical operations in SAT/SMT solving. In some situations, the solver may choose a decision variable between one corresponding to the axiom applied in some proof step and one corresponding to the instantiation. We expect that often it would be beneficial to choose the former. Such guiding information could be possibly also gathered by a controlled application of forward-chaining. This would require modifying both the communication between the CL prover and SAT/SMT solvers, and the SAT/SMT solvers themselves.

Applications in other domains

We are planning to use the presented approach to some other logics (not only CL), especially those without good available decision or semi-decision procedures. Also, we will try to apply the presented approach to complex symbolic computations that can be presented in a similar manner to proofs, such as computing Gröbner bases or solving the Rubik's cube.

Conclusions

We presented an approach for automated theorem proving and for automated construction of proof objects based on constraint solving (i.e., a new paradigm that we can call "theorem proving as constraint solving"). That idea is not surprising or completely unexpected (especially given many other kinds of problems tackled by constraint solving), but still it has almost no mentions in the literature. One may only speculate why it is so. Maybe it was expected that this approach would be unfeasible and without practical usability.

Our work shows that, for an interesting and expressible fragment of FOL, the approach is feasible and, moreover, that it has some unique merits and features such as: producing all proofs; producing shortest proofs; producing natural-looking proofs expressed in a forward reasoning manner -both in a natural language form and in a form verifiable by interactive provers and readable at the same time; producing even more compact proofs using inlining, using hints about a proof to be found, etc.

We find that the proposed approach and the presented prover can be useful especially in the context of formalisation of mathematical theories and as a support in interactive theorem proving. Our prototype implementation gives reasonable performance especially when compared to provers producing proofs verifiable by a proof assistant.

In the area of automated theorem proving without construction of verifiable proofs, the presented approach faces a strong competition in FOL provers. They have been evolving for more than half a century, they often combine several underlying strategies or provers using portfolio approach and it is hard to beat their performances . However, beating performance of the leading FOL provers is not one of the targets of our approach -it is rather complementary with the FOL provers and has different main merits. In addition, there is a number of other logical frameworks where solvers and reasoners are not so well developed and the approach presented here could easily lead to practically usable automated theorem provers -one needs only a precise notion of proof or a solution (which could take only a few hundreds lines, as shown for CL) and encoding to a sequence of natural numbers. An ultimate target would be a generic framework that automatically prove theorems, given only a precise notion of a proof in the underlying logic and theory. The approach could be applied to virtually any underlying logic and theory with a precise syntactical notion of proof. However, although it would be possible, it would be challenging to encode proof steps involving non-trivial features such as unification, or Fourier/Motzkin elimination [START_REF] Imbert | Fourier's Elimination: Which to Choose? In Principles and Practice of Constraint Programming[END_REF], or elimination steps used in the area method [START_REF] Janičić | The Area Method : a Recapitulation[END_REF]. And not only the encoding, but also the efficiency of such proving procedure would be also questionable. On the other hand, the approach is very suitable for syntactically simple theories and proofs, such are propositional calculi and coherent logic. Indeed, the current version of the presented approach, applied here to coherent logic, enjoys a suitable simplicity: it does not support function symbols. The presented encoding has to be significantly extended to make function symbols usable. Alternatively, problems involving function symbols could be encoded using predicate symbols only, but that would make generated proofs longer and less readable.

In summary, we believe that "theorem proving as constraint solving" work presented in this paper is a first encouraging attempt, leaving room for further improvements and a range of applications. T h e r e f o r e t h e r e i s no i n t e r p r e t a t i o n t h a t makes a l l g i v e n c l a u s e s s i m u l t a n e o u s l y f a l s e . Hence t h e g i v e n c l a u s e s a r e v a l i d . q . e . d .

A.2 Nanocop

Γ

  , ax, A 0 ( a), . . . , A n-1 ( a), B 0 ( a, b) ∨ . . . ∨ B m-1 ( a, b) P Γ, ax, A 0 ( a), . . . , A n-1 ( a) P MP Γ, B 0 ( c) P . . . Γ, B m-1 ( c) P Γ, B 0 ( c) ∨ . . . ∨ B m-1 ( c) P QEDcs (case split) Γ, B i ( a, b) ∃ y(B 0 ( a, y) ∨ . . . ∨ B m-1 ( a, y))

  replaced by the conjecture: ∀x∃y (a(x) ⇒ (b or c and d or e(x, y))) and the following additional axioms: ∀x (c(x) ∧ d(x) ⇒ c and d(x)) ∀x, y (b(x, y) ⇒ b or c and d or e(x, y)) ∀x, y (c and d(y) ⇒ b or c and d or e(x, y)) ∀x, y (e(y) ⇒ b or c and d or e(x, y))

  y)) has been applied. It has been instantiated using an instantiation σ = [ x → a, y → b]. Constants b are new, fresh constants (not present in the original signature), and all the facts A 0 ( a), . . . A n-1 ( a) have been proved previously, on the current proof branch. FirstCase : There is a preceding MP step with a conclusion B 0 ( a, b) ∨ B 1 ( a, b).

Example 4

 4 Consider again the CL proof shown in Example 1:Consider an arbitrary a such that: p(a). It should be proved that r(a).

Example 7

 7 Let us again consider the proof given as a sequence of numbers in Section 3

Fig. 1

 1 Fig. 1 Comparing different parameters for Larus

Fig. 2

 2 Fig. 2 Experimental results for Euclid's Elements benchmarks

Fig. 3

 3 Fig.3Percentage of lemmas proved within 100s compared to the length of the handcrafted formal proof.

Fig. 4

 4 Fig. 4 Experimental results for coherent logic benchmarks

Fig. 5

 5 Fig. 5 Number of problem solved in less than some given time on the col-trans corpus

Fig. 6

 6 Fig. 6 Number of problem solved in less than some given time on the crafted corpus

Example 8

 8 Consider the axiom r(a) ∨ r(b) and the conjecture r(b) ∨ r(a). It has the following proof of length 6: It should be proved that r(b) ∨ r(a).

  1. r(a) ∨ r(b) (by MP, using axiom ax1) 2. Case r(a): 3. Proved by assumption! (by QEDas) 4. Case r(b): 5. Proved by assumption! (by QEDas) 6. Proved by case split! (by QEDcs, by r(a), r(b))

1 .

 1 r(b, a) (by MP, from p(a, b) using axiom ax1; instantiation: A → a, B → b) 2. r(a, b) (by MP, from r(b, a) using axiom ax3; instantiation: A → b, B → a) 3. p(b, a) (by MP, from r(a, b) using axiom ax4; instantiation: A → a, B → b) 4. Proved by assumption! (by QEDas)

Fig. 7

 7 Fig. 7 Euclid's Proposition 43: the areas of the two shaded parallelograms are equal.

  proposition 04).Consider arbitrary a, b, c such that: isosceles(a, b, c). It should be proved that congA(a, b, c, a, c, b).

1 .

 1 col(c, a, b) ∨ ¬col(c, a, b) (by MP, using axiom cn col1b; instantiation: A → c, B → a, C → b) 2. Case col(c, a, b): 3. ⊥ (by MP, from col(c, a, b), isosceles(a, b, c) using axiom nnncolNegElim; instantiation: A → a, B → b, C → c) 4. Contradiction! (by QEDefq) 5. Case ¬col(c, a, b): 6. congA(a, b, c, a, c, b) (by MP, from isosceles(a, b, c), isosceles(a, b, c), ¬col(c, a, b) using axiom proposition 04; instantiation: A → a, B → c, C → b, Xa → a, Xb → b, Xc → c) 7. Proved by assumption! (by QEDas) 8. Proved by case split! (by QEDcs, by col(c, a, b), ¬col(c, a, b))

HHHHH

  The triangles AEI and AHI have equal areas because they are congruent, because AHIE is a parallelogram (implicit step).The triangles ABC and ADC have equal areas because they are congruent, because ADCB is a parallelogram (implicit step).The quadrilateral HDCI and EICB have equal areas which can be deduced from the two previous implicit steps using the axiom cutoff1.The triangles IGC and IF C have equal areas because they are congruent, because GIF C is a parallelogram (implicit step).The conclusion can be deduced from the previous steps using the axiom cutoff2.

Fig. 8

 8 Fig. 8 Euclid's Proposition 43: details of the proofs steps, three proof steps are implicit in the proof generated by Larus.

[

  -( congA ( 1 ˆ[ ] , 2 ˆ[ ] , 3 ˆ[ ] , 1 ˆ[ ] , 3 ˆ[ ] , 2 ˆ[ ] ) ) , c o n g ( 1 ˆ[ ] , 2 ˆ[ ] , 1 ˆ[ ] , 3 ˆ[ ] ) , c o n g ( 1 ˆ[ ] , 3 ˆ[ ] , 1 ˆ[ ] , 2 ˆ[ ] ) ] 2 . 1 . 1 . 1 Assume -(congA ( 1 ˆ[ ] , 2 ˆ[ ] , 3 ˆ[ ] , 1 ˆ[ ] , 3 ˆ[ ] , 2 ˆ[ ] ) ) i s f a l s e .Then c l a u s e ( 2 ) i s t r u e .2 . 1 . 1 . 2 Assume c o n g ( 1 ˆ[ ] , 2 ˆ[ ] , 1 ˆ[ ] , 3 ˆ[ ] ) i s f a l s e .Then c l a u s e (4) u n d e r t h e s u b s t i t u t i o n [ [ 5 [ ] , 1 ˆ[ ] ] ] i s f a l s e i f a t l e a s t o n e o f t h e f o l l o w i n g i s f a l s e : [ i s o s c e l e s ( 1 ˆ[ ] , 2 ˆ[ ] , 3 ˆ[ ] ) ] 2 . 1 . 1 . 2 . 1 Assume i s o s c e l e s ( 1 ˆ[ ] , 2 ˆ[ ] , 3 ˆ[ ] ) i s f a l s e . Then c l a u s e ( 1 ) i s t r u e . 2 . 1 . 1 . 3 Assume c o n g ( 1 ˆ[ ] , 3 ˆ[ ] , 1 ˆ[ ] , 2 ˆ[ ] ) i s f a l s e . Then c l a u s e ( 6 ) u n d e r t h e s u b s t i t u t i o n [ [ 6 [ ] , 1 ˆ[ ] , 3 ˆ[ ] , 1 ˆ[ ] ] ] i s f a l s e i f a t l e a s t o n e o f t h e f o l l o w i n g i s f a l s e : [ c o n g ( 1 ˆ[ ] , 2 ˆ[ ] , 1 ˆ[ ] , 3 ˆ[ ] ) ] 2 . 1 . 1 . 3 . 1 Assume c o n g ( 1 ˆ[ ] , 2 ˆ[ ] , 1 ˆ[ ] , 3 ˆ[ ] ) i s f a l s e . T h i s a s s u m p t i o n h a s b e e n r e f u t e d i n 2 . 1 . 1 . 2 .

A. 6 Larus

 6 t p t p-p r o b l e m s / e u c l i d -n a t i v e -e q / 0 1 5 p r o p o s i t i o n 0 5 . p i s a Theorem S t a r t o f p r o o f f o r t p t p-p r o b l e m s / e u c l i d -n a t i v e -e q / 0 1 5 p r o p o s i t i o n 0 5 . p [ ( 2 6 ˆ0 ) ˆ[ 8 3 ˆ[ ] , 82 ˆ[ ] , 81 ˆ[ ] ] : [ t r i a n g l e ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 [ ] ) , c o l ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 ˆ[ ] ) ] , [ ( 2 ˆ1 ) ˆ[ 8 3 ˆ[ ] , 82 ˆ[ ] , 81 ˆ[ ] ] : [ -( t r i a n g l e ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 ˆ[ ] ) ) , 5 ˆ1 : [ ( 6 ˆ1 ) ˆ[ ] : [ ] ] , i s o s c e l e s ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 ˆ[ ] ) ] , [ ( 8 5 ˆ2 ) ˆ[ ] : [ -( i s o s c e l e s ( 8 1 ˆ[ ] ,82ˆ[ ] , 83 ˆ[ ] ) ) ] ] ] , [ ( 3 8 ˆ1 ) ˆ[ 8 3 ˆ[ ] , 81 ˆ[ ] , 82 ˆ[ ] ] : [ -( c o l ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 ˆ[ ] ) ) , 41 ˆ1 : [ ( 4 2 ˆ1 ) ˆ[ ] : [ ] ] , c o l ( 8 2 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] ) ] , [ ( 5 2 ˆ2 ) ˆ[ 8 3 ˆ[ ] , 81 ˆ[ ] , 82 ˆ[ ] ] : [ -( c o l ( 8 2 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] ) ) , -(congA ( 8 2 ˆ[ ] , 81 ˆ[ ] , 83 [ ] , 83 [ ] , 81 ˆ[ ] , 82 ˆ[ ] ) ) ] , [ ( 5 8 ˆ3 ) ˆ[ 8 2 ˆ[ ] , 83 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] , 82 ˆ[ ] , 81 ˆ[ ] ] : [ congA ( 8 2 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] , 83 ˆ[ ] , 81 ˆ[ ] , 82 ˆ[ ] ) ,69 3 : [ ( 7 0 ˆ3 ) ˆ[ ] : [ -( c o n g ( 8 2 ˆ[ ] , 83 ˆ[ ] , 83 ˆ[ ] , 82 ˆ[ ] ) ) ] , ( 7 2 ˆ3 ) ˆ[ ] : [ -( congA ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] , 82 ˆ[ ] ) ) ] , ( 7 4 ˆ3 ) [ ] : [ -( congA ( 8 1 ˆ[ ] , 8 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] ) , c o n g ( 8 1 ˆ[ ] , 83 ˆ[ ] , 81 ˆ[ ] , 82 ˆ[ ] ) ] , [ ( 8 7 6 ) ˆ[ ] : [ congA ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] , 82 ˆ[ ] ) ] ] , [ ( 2 ˆ4 ) [ 8 3 ˆ[ ] , 82 ˆ[ ] , 81 ˆ[ ] ] : [ -( c o n g ( 8 1 ˆ[ ] , 82 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] ) ) , 5 ˆ4 : [ ( 8 ˆ4 ) ˆ[ ] : [ ] ] , i s o s c e l e s ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 ˆ[ ] ) ] , [ ( 8 5 ˆ5 ) ˆ[ ] : [ -( i s o s c e l e s ( 8 1 ˆ[ ] , 82 ˆ[ ] , 83 ˆ[ ] ) ) ] ] ] , [ ( 2 0 ˆ4 ) ˆ[ 8 3 ˆ[ ] , 82 ˆ[ ] , 81 ˆ[ ] , 81 ˆ[ ] ] : [ -( c o n g ( 8 1 ˆ[ ] , 83 ˆ[ ] , 81 ˆ[ ] , 82 ˆ[ ] ) ) , c o n g ( 8 1 ˆ[ ] , 82 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] ) ] , [ 1 6 5 8 5 ˆ1 6 5 8 6 : [ -( c o n g ( 8 1 ˆ[ ] , 82 ˆ[ ] , 81 ˆ[ ] , 83 ˆ[ ] ) ) ] ] ] ] ] ] ] End o f p r o o f f o r t p t p-pr o b l e m s / e u c l i d -n a t i v e -e q / 0 1 5 p r o p o s i t i o n 0 5 . p g e n e r a l i z e ( z e n o n H 3 4 zen on T A p ) . z e n o n i n t r o z e n o n H 3 8 . a p p l y ( z e n o n i m p l y s z e n o n H 3 8 ) ; [ z e n o n i n t r o z e n o n H 3 a | z e n o n i n t r o z e n o n H 3 9 ] . g e n e r a l i z e ( z e n o n H 3 5 zen on T A p ) . z e n o n i n t r o z e n o n H 3 b . g e n e r a l i z e ( z e n o n H 3 7 z e n o n T B o ) . z e n o n i n t r o z e n o n H 3 c . a p p l y ( z e n o n i m p l y s z e n o n H 3 c ) ; [ z e n o n i n t r o z e n o n H 3 e | z e n o n i n t r o z e n o n H 3 d ] . g e n e r a l i z e ( z e n o n H 3 b z e n o n T C n ) . z e n o n i n t r o z e n o n H 3 f . a p p l y ( z e n o n i m p l y s z e n o n H 3 f ) ; [ z e n o n i n t r o z e n o n H 4 1 | z e n o n i n t r o z e n o n H 4 0 ] . e x a c t ( z e n o n H 4 1 z e n o n H 3 2 ) . a p p l y ( z e n o n a n d s z e n o n H 4 0 ) . z e n o n i n t r o z e n o n H 4 3 . z e n o n i n t r o z e n o n H 4 2 . a p p l y ( z e n o n a n d s z e n o n H 4 2 ) . z e n o n i n t r o z e n o n H 4 5 . z e n o n i n t r o z e n o n H 4 4 . e x a c t ( z e n o n H 3 e z e n o n H 4 5 ) . a p p l y ( z e n o n a n d s z e n o n H 3 d ) . z e n o n i n t r o z e n o n H 4 7 . z e n o n i n t r o z e n o n H 4 6 . a p p l y ( z e n o n a n d s z e n o n H 4 6 ) . z e n o n i n t r o z e n o n H 4 9 . z e n o n i n t r o z e n o n H 4 8 . e x a c t ( z e n o n H 3 a z e n o n H 4 9 ) . a p p l y ( z e n o n a n d s z e n o n H 3 9 ) . z e n o n i n t r o z e n o n H 4 b . z e n o n i n t r o z e n o n H 4 a . a p p l y ( z e n o n a n d s z e n o n H 4 a ) . z e n o n i n t r o z e n o n H 3 2 . z e n o n i n t r o z e n o n H 4 c . a p p l y ( z e n o n a n d s z e n o n H 4 c ) . z e n o n i n t r o z e n o n H 4 5 . z e n o n i n t r o z e n o n H 4 d . a p p l y ( z e n o n a n d s z e n o n H 4 d ) . z e n o n i n t r o z e n o n H 4 7 . z e n o n i n t r o z e n o n H 4 3 . g e n e r a l i z e ( d e f t r i a n g l e ze non TA p ) . z e n o n i n t r o z e n o n H 4 e . g e n e r a l i z e ( z e n o n H 4 e z e n o n T B o ) . z e n o n i n t r o z e n o n H 4 f . g e n e r a l i z e ( z e n o n H 4 f z e n o n T C n ) . z e n o n i n t r o z e n o n H 5 0 . a p p l y ( z e n o n i m p l y s z e n o n H 5 0 ) ; [ z e n o n i n t r o z e n o n H 5 2 | z e n o n i n t r o z e n o n H 5 1 ] . g e n e r a l i z e ( d e f i s o s c e l e s zen on T A p ) . z e n o n i n t r o z e n o n H a . g e n e r a l i z e ( z e n o n H a z e n o n T B o ) . z e n o n i n t r o z e n o n H 1 0 . g e n e r a l i z e ( z e n o n H 1 0 z e n o n T C n ) . z e n o n i n t r o z e n o n H 1 1 . a p p l y ( z e n o n i m p l y s z e n o n H 1 1 ) ; [ z e n o n i n t r o z e n o n H 1 3 | z e n o n i n t r o z e n o n H 1 2 ] . e x a c t ( z e n o n H 1 3 z e n o n H c ) . a p p l y ( z e n o n a n d s z e n o n H 1 2 ) . z e n o n i n t r o z e n o n H 1 5 . z e n o n i n t r o z e n o n H 1 4 . e x a c t ( z e n o n H 5 2 z e n o n H 1 5 ) . e x a c t ( z e n o n H 5 1 z e n o n H 4 3 ) . e x a c t ( z e n o n H 2 d z e n o n a p p l y ( z e n o n a n d s z e n o n H 2 a ) . z e n o n i n t r o z e n o n H 5 4 . z e n o n i n t r o z e n o n H 5 3 . a p p l y ( z e n o n a n d s z e n o n H 5 3 ) . z e n o n i n t r o z e n o n H 5 6 . z e n o n i n t r o z e n o n H 5 5 . e x a c t ( z e n o n H 2 2 z e n o n H 5 6 ) . Qed . Not minimal proof: Theorem p r o p o s i t i o n 0 5 : f o r a l l A B C : MyT, i s o s c e l e s A B C -> congA A B C A C B . P r o o f . i n t r o s c a cb c c . i n t r o s . a s s e r t ( c o l c a cb c c \/ ˜c o l c a cb c c ) by a p p l y i n g ( c n c o l 1 b c a cb c c ) . by c a s e s on ( ( c o l c a cb c c ) \/ ( ˜c o l c a cb c c ) ) . -{ a s s e r t ( t r i a n g l e c a cb c c ) by a p p l y i n g ( d e f i s o s c e l e s c a cb c c ) . a s s e r t ( ˜c o l c a cb c c ) by a p p l y i n g ( d e f t r i a n g l e c a cb c c ) . a s s e r t ( c o l c a c a c a \/ ˜c o l c a c a c a ) by a p p l y i n g ( c n c o l 1 b c a c a c a ) . by c a s e s on ( ( c o l c a c a c a ) \/ ( ˜c o l c a c a c a ) ) . -{ a s s e r t ( F a l s e ) by c o n t r a d i c t i o n o n ( c o l c a cb c c ) . c o n t r a d i c t . } -{ a s s e r t ( ˜c o l c a cb c c ) by a p p l y i n g ( d e f t r i a n g l e c a cb c c ) . a s s e r t ( F a l s e ) by c o n t r a d i c t i o n o n ( c o l c a cb c c ) . c o n t r a d i c t . } } -{ a s s e r t ( c o l c c c a cb \/ ˜c o l c c c a cb ) by a p p l y i n g ( c n c o l 1 b c c c a cb ) . by c a s e s on ( ( c o l c c c a cb ) \/ ( ˜c o l c c c a cb ) ) .

  MP : One of the given axioms AX has been applied, i.e., the following conditions are met for some k, 0 ≤ k < |AX |, where the k-th axiom is:A 0 ( x) ∧ . . . ∧ B 0 ( a, b) and, if m = 2, Contents (s)(1) = B 1 ( a, b); 7.The mapping From (s)(i) maps each i, 0 ≤ i < n to one of numbers s , such that 0 ≤ s < s and such that in the s -th proof step the fact A i ( a) was derived. In addition, it must hold that: -Cases (s ) = false (s must not be branching step, it must contain a single fact, not a disjunction of two); -the steps s and s are on the same proof branch.8

	2. Cases (s) = false; QEDbyAssumption :
	3. Nesting (s) = 1; 1. StepKind (s) = QEDbyAssumption ;
	4. Contents (s)(0) = As( a) 2. s > 0;
	3. Goal (s -1); 9
	4. Goal (s);
	A n-1 ( x) ⇒ ∃ y(B 0 ( x, y) ∨ . . . ∨ B m-1 ( x, y)) (where m is 1 or 2): 5. Nesting (s) = Nesting (s -1).
	1. StepKind (s) = MP ; QEDbyEFQ :
	2. AxiomApplied (s) = k; 1. StepKind (s) = QEDbyEFQ ;
	3. There is a finite mapping Instantiation (s) that maps each quantified vari-2. s > 0;
	able from x to a constant: Instantiation (s)(x i ) = a i and also from y i to a 3. Contents (s -1)(0) = ⊥;
	new, fresh constant: Instantiation (s)(y i ) = b i (other arguments of atomic 4. Goal (s);
	formulae are constants); 5. Nesting (s) = Nesting (s -1).
	4. Cases (s) = false, iff m equals 1;
	5. Nesting (s) = Nesting (s -1), if s > 0, otherwise Nesting (s) = 1;
	6. Contents (s)(0) = FirstCase :
	1. StepKind (s) = FirstCase ;
	2. s > 0;
	3. StepKind (s -1) = MP ;
	4. Cases (s -1) = true;
	5. Cases (s) = false;
	6. Nesting (s) = 2• Nesting (s -1);
	7. Contents (s)(0) = Contents (s -1)(0).
	SecondCase :
	1. StepKind (s) = SecondCase ;
	2. s > 0;
	3. the step s -1 is one of the QED steps;
	4. there is a step s , 0 ≤ s < s -2 such that;
	-StepKind (s ) = MP ;
	-Cases (s ) = true;
	-Contents (s)(0) = Contents (s )(1);
	5. Cases (s) = false;
	6. Nesting (s) =Nesting (s -1) + 1.
	QEDbyCases :
	1. StepKind (s) = QEDbyCases ;
	2. s > 0;
	3. the step s -1 is one of the QED steps;
	4. Goal (s);
	5. Nesting (s -1) is odd;
	6. Nesting (s) = (Nesting (s -1) -1)/2.
	1. StepKind (s) = Assumption ;

https://github.com/janicicpredrag/URSA

Transformation to CL2 differs for axioms and for conjectures, because they have different polarity in the proving context: axioms conjecture.

The given content, i.e., a proof represented by numbers, was created automatically by our prover. The shown proof representation does not include all variables that were considered during the proving/solving process. Also, some of the given values are redundant (but are still kept for convenience in this representation).

The way we represent this condition is described in Section 4.

For the very first proof step following the given assumptions, there should be also a constraint corresponding to a posibility that the goal has been met by some of the given assumptions.

Even if there are broadly available SAT and SMT solvers which have been tested on a large amount of problems by a large amount of users and even some integrated in interactive proof assistant using either a reflexive approach or one based on checking certificates, we think it is simpler to use the final reconstructed proof for the original statement as a certificate.

https://code.google.com/archive/p/clp/source

https://geocoq.github.io/GeoCoq/

Note that in the Coq files generated from TPTP files, the statements are not curryfied. We noticed that this reduces the efficiency of the Coq tactics.

For this corpus, Larus is used with options: no case splits, start by looking for a proof of at most 2 steps, do not use negation elimination . Proof verification using Coq is not used for this corpus (only for this corpus the time needed for proof verification is not negligible).

Acknowledgements

We are grateful to the anonymous reviewers who gave us a very useful feedback and number of suggestions that significant improved the earlier version of this paper.

A Example proofs of Proposition 5

In this section, we list the proofs of Euclid Book 1, Proposition 5, generated by different theorem provers. ------------------------------------------------------E x p l a n a t i o n s f o r t h e p r o o f p r e s e n t e d b e l o w : t o s o l v e u n s a t i s f i a b l e p r o b l e m s t h e y a r e n e g a t e d e q u a l i t y a x i o m s a r e added i f r e q u i r e d t e r m s and v a r i a b l e s a r e r e p r e s e n t e d by P r o l o g t e r m s and P r o l o g v a r i a b l e s , n e g a t i o n i s r e p r e s e n t e d by --I ˆ[ t 1 , . . , t n ] r e p r e s e n t s t h e atom P I ( t 1 , . . , t n ) o r t h e Skolem term f I ( t 1 , t 2 , . . , t n ) i n t r o d u c e d d u r i n g t h e c l a u s a l f o r m t r a n s l a t i o n t h e s u b s t i t u t i o n [ [ X1 , . . , Xn ] , [ t 1 , . . , t n ] ] r e p r e s e n t s t h e a s s i g n m e n t s X1:= t 1 , . . , Xn:= t n P r o o f :

A.1 Leancop

------T r a n s l a t i o n i n t o ( d i s j u n c t i v e ) c l a u s a l f o r m : [START_REF] Alrabbaa | Finding Small Proofs for Description Logic Entailments: Theory and Practice[END_REF] [ -( i s o s c e l e s ( 1

[ i s o s c e l e s ( 4 9 1 6 , 4 9 7 6 , 5 0 3 5 ) , -( t r i a n g l e ( 4 9 1 6 , 4 9 7 6 , 5 0 3 5 ) ) ] ( 4 )

[ i s o s c e l e s ( 4 9 1 6 , 4 9 7 6 , 5 0 3 5 ) , -( c o n g ( 4 9 1 6 , 4 9 7 6 , 4 9 1 6 , 5 0 3 5 ) ) ] [START_REF] Beeson | Proof-checking Euclid[END_REF] [ -( i s o s c e l e s ( 5 4 8 1 , 5 5 4 1 , 5 6 0 0 ) ) , t r i a n g l e ( 5 4 8 1 , 5 5 4 1 , 5 6 0 0 ) , c o n g ( 5 4 8 1 , 5 5 4 1 , 5 4 8 1 , 5 6 0 0 ) ] [START_REF] Bezem | Newman's Lemma -a Case Study in Proof Automation and Geometric Logic[END_REF] [ c o n g ( 6 1 0 5 , 6 1 6 3 , 6 0 4 6 , 6 2 2 0 ) , -( c o n g ( 6 0 4 6 , 6 2 2 0 , 6 1 0 5 , 6 1 6 3 ) ) ] [START_REF] Bezem | Automating Coherent Logic[END_REF] [ t r i a n g l e ( 6 5 9 7 , 6 6 5 1 , 6 7 0 4 ) , c o l ( 6 5 9 7 , 6 6 5 1 , 6 7 0 4 ) ] [START_REF] Bezem | On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic[END_REF] [ -( c o l ( 7 0 0 6 , 7 0 6 0 , 7 1 1 3 ) ) , -( t r i a n g l e ( 7 0 0 6 , 7 0 6 0 , 7 1 1 3 ) ) ] ( 9 We p r o v e t h a t t h e g i v e n c l a u s e s a r e v a l i d , i . e . f o r a g i v e n s u b s t i t u t i o n t h e y e v a l u a t e t o t r u e f o r a l l i n t e r p r e t a t i o n s . The p r o o f i s by c o n t r a d i c t i o n : Assume t h e r e i s an i n t e r p r e t a t i o n s o t h a t t h e g i v e n c l a u s e s e v a l u a t e t o f a l s e . Then i n e a c h c l a u s e t h e r e h a s t o be a t l e a s t o n e l i t e r a l t h a t i s f a l s e .

Then c l a u s e [START_REF] Bezem | Automating Coherent Logic[END_REF]

Then c l a u s e ( 1 4 ) u n d e r t h e s u b s t i t u t i o n [ [ 8 4 5 5 , 8 3 9 9 , congA(σ0(a0), σ1(a0), σ2 (a0), σ0(a0), σ2(a0), σ1(a0)) ¬congA(σ0 (a0), σ1(a0), σ2(a0), σ0 (a0), σ2(a0), σ1(a0)) isosceles(σ0(a0), σ1(a0), σ2 (a0)) ∧ ¬congA(σ0 (a0), σ1(a0), σ2(a0), σ0(a0), σ2(a0), σ1 (a0))

¬congA(σ0 (a0), σ1(a0), σ2(a0), σ0 (a0), σ2(a0), σ1

[13, 24

→ (isosceles (σ0 (a0),

A.7 Isabelle

Isabelle 2016 generated several proof using Sledgehammer. The first proof is the most informative but we can still feel that the proof has been converted from resolution proof. Moreover, the generated proof is not accepted by Isabelle. The second proof is accepted by not very informative. The third proof is a one-liner calling the meeson tactic.

A.8 Manual formal proof in Coq

For comparison, we provide the original Coq proof: