A Syntax for Connection Proofs Jens Otten1 , Sean B. Holden2 1 Department of Informatics, University of Oslo, Norway 2 Department of Computer Science and Technology, University of Cambridge,United Kingdom Abstract Providing a proof certificate is one of the most important features of (fully automated) theorem proving systems. For theorem provers based on, e.g, resolution or superposition calculi, a syntax for writing solutions is well documented and used. Even though attempts have been made to specify a syntax for connection calculi, there is currently no such syntax in common use. This paper provides an overview of the proof syntax used by existing connection provers and proposes an improved syntax for connection proofs. Due to the general approach, the syntax can be extended to also represent connection proofs in some non-classical logics. Keywords Automated Reasoning, logic, connection calculus, connection proofs, syntax, TPTP, proof certificate 1. Introduction One of the most important features of automated theorem proving (ATP) systems is the output of a proof certificate, which contains a detailed description of the proof and that can be verified by an external (independent) tool. Representing these proofs in a standardized format increases the interoperability between ATP systems, ATP tools, and application software. Such ATP tools can, for example, be used to represent found proofs in a more readable form. The writing of derivations in resolution calculi using the TPTP/TSTP syntax is well docu- mented and specified [20]. For many other calculi, such as connection or sequent calculi, such a common specification does not exist. Derivations in these calculi differ significantly from derivations in the resolution calculus. Whereas the leaves of a proof in the (formal) connection calculus consist of the axioms of the calculus, the leaves of a (TSTP) derivation in the resolution calculus consist of the axiom formulae of the given problem. This paper proposes a syntax for connection proofs. It should not be seen as a final specifica- tion, but as a foundation to initiate discussions within the community in order to finalize such a specification. We start with a description of the requirements for a standardized syntax (Section 2), before presenting details of existing syntaxes for proofs, including the well-known TPTP syntax and the syntaxes used by the connection provers leanCoP and Connect++ (Section 3). Afterwards, we specify our proposed syntax for connection proofs (Section 4), before concluding with a summary and outlook (Section 5). AReCCa 2023: Automated Reasoning with Connection Calculi, 18 September 2023, Prague, Czech Republic $ jeotten@ifi.uio.no (J. Otten); sbh11@cl.cam.ac.uk (S. B. Holden) € http://jens-otten.de/ (J. Otten); http://www.cl.cam.ac.uk/~sbh11 (S. B. Holden)  0000-0002-4331-8698 (J. Otten); 0000-0001-7979-1148 (S. B. Holden) © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) AReCCa 2023 84 CEUR-WS.org CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings 2. Preliminaries We describe requirements for a proof syntax and introduce the formal connection calculus. 2.1. Requirements for a Proof Syntax There are certain requirements that a proof syntax should fulfill in order be widely accepted by the community. These are: • Simple/lean: The syntax should be as concise and simple as possible allowing a natural and straightforward representation of proofs. A proof syntax that is appropriate for one calculus might not be suitable to represent proofs in another calculus. • Human-readable: Even though one of the main purposes of a standardized proof syntax is the interoperability between ATP systems, ATP tools and application software, a proof in such a syntax should be readable by a human. • Based on established formats: The proof syntax should consider the syntaxes of previous proof formats, whenever these can be used in a straightforward way and do not make the proof representation more complicated than necessary (see first requirement). • Well documented and specified: The proof syntax should be described in a concise and unambiguous way. • Extendable: The proof syntax should be kept general enough to be extendable to similar or related proof calculi, for example for non-classical logics. • Efficiently verifiable: It should be possible to verify the correctness of a given “proof” in at most polynomial time. This excludes, for example, “proofs” consisting only of a set of unsatisfiable clauses, for which finding a real proof is NP-complete. In general, a proof of (the validity of) a first-order formula F is a proof of F in a (correct) proof calculus. We will focus on the clausal connection calculus. 2.2. The Connection Calculus Connection calculi, such as the connection method [2], the connection tableau calculus [8] and the model elimination calculus [9], are established proof search calculi. We use the standard language of classical first-order logic. A (first-order) formula (denoted by F ) is built up from atomic formulae, denoted by A, the connectives ¬, ∧, ∨, ⇒, and the first-order quantifiers ∀ and ∃. A literal L has the form A or ¬A. In the clausal connection calculus [2, 14] a formula is represented as a matrix. The (classical) matrix M (F ) of a formula F is its representation as a set/list of clauses, where each clause is a set/list of literals. It is the representation of F in disjunctive normal form. Skolemization of the Eigenvariables is done in the usual way. In the graphical representation of a matrix, its clauses are arranged horizontally, while the literals of each clause are arranged vertically. In contrast to sequent calculi [5] and (standard) tableau calculi, the proof search in connection calculi is guided by connections. A connection is a set {A1 , ¬A2 } of literals with the same atomic formula, but different polarities. A term substitution σ assigns terms to variables. A connection {A1 , ¬A2 } is σ-complementary iff σ(A1 ) = σ(A2 ). 85 C2 , M, {} Axiom (A) Start (S) C2 is a copy of C1 ∈M {}, M, P ath ε, M, ε C, M, P ath∪{L2 } Reduction (R) {L1 , L2 } is σ-complementary C∪{L1 }, M, P ath∪{L2 } C2 \{L2 }, M, P ath∪{L1 } C, M, P ath C2 is a copy of C1 ∈M , L2 ∈C2 , Extension (E) C∪{L1 }, M, P ath {L1 , L2 } is σ-complementary Figure 1: The clausal connection calculus for classical logic. The connection calculus has the three inference rules Start, Reduction, Extension, and one Axiom. It is shown in Figure 1; for details see [2, 8, 14, 11]. The words of the calculus are tuples “C, M, Path”, where M is a matrix, C is a (subgoal) clause or ε and (the active) Path is a set of literals or ε. A copy of a clause C is made by renaming all variables in C. The rigid term substitution σ is calculated by using one of the well-known term unification algorithms whenever a connection is identified. The connection calculus is sound and complete [2]. Definition 1 (Connection Proof). A connection proof of M is a derivation of ε, M, ε with a term substitution σ in the connection calculus, in which all leaves are closed by axioms. Example 1. A slightly simplified version1 of Pelletier’s problem 24 [17], called Pelletier 24a, consists of the following four axioms2 and one conjecture formulae.3 ∃x(P x ∧ Rx) Conjecture {P x, Rx} (1) ¬(∃x(Sx ∧ Qx)) Axiom 1 {Sy, Qy} (2) ∃xP x Axiom 3a {¬P a} (3) ∀x(Qx ⇒ Sx) Axiom 4a {Qv, ¬Sv} (4) ∀(P x ⇒ (Qx ∨ Rx)) Axiom 2 {P z, ¬Qz, ¬Rz} (5) Translating these formulae into clausal form (shown in the third column4 ) results in the matrix Ma = {{P x, Rx}, {Sy, Qy}, {¬P a}{Qv, ¬Sv}, {P z, ¬Qz, ¬Rz}}. The connection proof for Ma is shown below. Its graphical matrix representation is shown in Figure 2. The proof steps are labeled with the number of the used clause C1 and the term substitution applied to it. A {}, Ma , {Rx, ¬Qv, Sy} R A {Qz}, Ma , {Rx, ¬Qv, Sy} {}, Ma , {Rx, ¬Qv} E (4, {z\a}) A {Sy}, Ma , {Rx, ¬Qv} {}, Ma , {Rx} A E (2, {y\a}) {}, Ma , {Rx, P v} {¬Qv}, Ma , {Rx} E (3) A {P v, ¬Qv}, Ma , {Rx} {}, Ma , {} A E (5, {v\a}) {}, Ma , {P x} {Rx}, Ma , {} E (3) {P x, Rx}, Ma , {} S (1, {x\a}) ε, Ma , ε 1 The original axioms 3 and 4 are ¬(∃xP x) ⇒ ∃yQy and ∀x((Qx ∨ Rx) ⇒ Sx) , respectively. 2 Note the difference between the axioms of the problem (the input formula) and the axiom of the calculus. 3 Axiom 2 is moved to the end of the set of axioms in order to comply with the proofs in Section 3. 4 A conjecture or axiom might result in more than one clause, which are marked with distinct numbers. 86  (1) ↓ (2) (4)  (1) [1, {x\a}] (7)  (2) [3]   Px Sy ¬P a Qz Pv   Px  Sy ¬P a Qz Pv   (3) [5, {v\a}]    (4) [3]   Rx Qy ¬Sz ¬Qv    Rx  Qy ¬Sz ¬Qv   (5) [2, {y\a}] (6) (6) [4, {z\a}]    ¬Rv ¬Rv (3) (5) (7) (R) Figure 2: A proof for Ma using the graphical matrix representation. 3. Existing Syntaxes for Connection Proofs We present the syntax used for the TPTP library and by the provers leanCoP and Connect++. 3.1. The TPTP/TSTP Syntax The TPTP and TSTP languages are suitable for representing problems and derivations in first- order and higher-order logic [19, 20]. The top level building blocks are of the following form: language(name,role,formula,source,useful_info). language is, for example, fof for first-order form or cnf for (conjunctive or disjunctive) clause normal form. Each formula has a unique name. role is a label such as axiom or conjecture. The source describes where the formula came from, for example an input file, and useful_info is a list of useful information. The last two fields are optional. Example 2. Pelletier’s original problem 24 is included as problem SYN054+1 in the TPTP library. The representation of its simplified version 24a from Example 1 in TPTP syntax is given in Figure 3. A derivation or proof written in the TPTP language is a list of annotated formulae, as for problems. For derivations/proofs the source has one of the forms file(file_name,file_info) inference(inference_name,inference_info,parents) The former is used for formulae taken from the problem file. The latter is used for inferred formulae, in which inference_name is the name of the inference rule, inference_info is a list of additional information about the inference, and parents is a list of the parents’ node names in the derivation. The inference_info contains items such as variable bindings captured within bind/2 terms. %------------------------------------------------------------------------ fof(pel24,conjecture, ( ? [X] : ( big_p(X) & big_r(X) ) )). fof(pel24_1,axiom, ( ~ ( ? [X] : ( big_s(X) & big_q(X) ) ) )). fof(pel24_2,axiom, ( ! [X] : ( big_p(X) => ( big_q(X) | big_r(X) ) ) )). fof(pel24_3a,axiom, ( ? [X] : big_p(X) )). fof(pel24_4a,axiom, ( ! [X] : ( big_q(X) => big_s(X) ) )). %------------------------------------------------------------------------ Figure 3: The presentation of Pelletier’s problem 24a in TPTP syntax, called SYN054a. 87 Table 1 The rules of the connection calculus using the connection tableau representation. Start Reduction Extension ✏✚✏❩ PP .. ✑◗ ✑ ◗ ✏ ✏✚ P . ✑ ◗ ✏ ✏ ✚ . . ❩ PP . ❩ P L. 2 ✑ ◗ L1 L2 . . . ... Ln .. ✑ L 1 ◗◗ ✑ ✏ ✏ P ✏PP ✏ ✏ ✚ ❙. P P ✏✏✚ ❙ P ❙. . . PP ✏ ✚ . . . ❙. . . PP C2 ={L1 , . . . , Ln } and ✏ ✏ ✚✚ . . P ✏ ✏ ✚ P C2 is copy of C1 ∈ M ′ L1 L2 ′ ... L1 . . . L′n ′ L1 L2 ′ ... L2 . . . L′n L2 is literal on path and L1 is leaf, C2 ={L′1 , . . . , L2 , . . . , L′n } {L1 , L2 } is σ-complementary and C2 is copy of C1 ∈ M , L2 ∈ C2 , {L1 , L2 } is σ-complementary 3.2. The leanCoP Syntax According to [20], a refutation (or proof) is a derivation that has the root node false, representing the empty clause. Whereas this description fits proofs in resolution calculi, it is not directly applicable to proofs in sequent, tableau or connection calculi. An attempt to “squeeze” connec- tion proofs into this resolution-style frame [15] resulted in a syntax that does not conform to the first two requirements suggested in Section 2.1: readability and simplicity. For this reason, leanCoP [14, 11] uses a syntax, called leanTPTP, that represents connection proofs in a more natural way, while still using main components of the TPTP/TSTP syntax. In order to shorten the output, leanCoP returns connection proofs in the connection tableau representation [8]. The rules of the connection tableau calculus are shown in Table 1 and correspond to the rules of the formal calculus in Figure 1. There is no explicit Axiom, which is applied exactly once for each Start or Extension step in the formal calculus. Instead, a derivation is a proof if each literal in a leaf is included in a σ-complementary connection {L1 , L2 }. Example 3. A proof of Pelletier’s problem 24a from Example 1 using the connection tableau representation is depicted in Figure 4. The rightmost literal in each proof step (number in parentheses) is annotated with the used clause number and (possibly) the term substitution that is applied to the clause. Proof step 1 is a Start step, step 7 is a Reduction step, all others are Extension steps. ✥✥❵❵❵❵ ✥ ✥ ✥✥✥ ❵❵❵ ✥✥ ❵❵ Px Rx (1) [1, {x\a}] ˂ ˂ ˂ ˂˂❍ ˂˂ ❈ ❍ ˂˂˂ ˂ ❈ ❍❍ ¬P a (2) [3] Pv ¬Qv ¬Rv (3) [5, {v\a}] (7) ❅ ❅ ¬P a (4) [3] Sy Qy (5) [2, {y\a}] ❅ ❅ Qz ¬Sz (6) [4, {z\a}] Figure 4: A proof for Ma using the connection tableau representation. 88 %----------------------------------------------------- cnf(1, plain, [big_p(X), big_r(X)], clausify(pel24)). cnf(2, plain, [big_s(X), big_q(X)], clausify(pel24_1)). cnf(3, plain, [-(big_p(a))], clausify(pel24_3a)). cnf(4, plain, [big_q(X), -(big_s(X))], clausify(pel24_4a)). cnf(5, plain, [big_p(X), -(big_q(X)), -(big_r(X))], clausify(pel24_2)). cnf(’1’,plain,[big_p(a),big_r(a)],start(1,bind([[X],[a]]))). cnf(’1.1’,plain,[-(big_p(a))],extension(3)). cnf(’1.2’,plain,[-(big_r(a)),big_p(a),-(big_q(a))],extension(5,bind([[X],[a]]))). cnf(’1.2.1’,plain,[-(big_p(a))],extension(3)). cnf(’1.2.2’,plain,[big_q(a),big_s(a)],extension(2,bind([[X],[a]]))). cnf(’1.2.2.1’,plain,[-(big_s(a)),big_q(a)],extension(4,bind([[X],[a]]))). cnf(’1.2.2.1.1’,plain,[-(big_q(a))],reduction(’1.2’)). %----------------------------------------------------- Figure 5: A proof of Pelletier’s problem 24a using the leanTPTP syntax as returned by leanCoP 2.2. A connection proof using the leanTPTP syntax is a list of proof steps of the form cnf(step_name,plain,clause,rule_info). in which step_name is the name of the proof step, clause is the used (instantiated) clause C2 , and rule_info has one of the following forms: start(clause_number,term_substitution) reduction(step_name) extension(clause_number,term_substitution) step_name is the name of the proof step and of the form ’N0 .N1 ....Nn ’, in which the Nn -th “open” literal L1 of its parent clause ’N0 .N1 ....Nn−1 ’ is used in a Reduction or Extension step; the name of the Start step ’N0 ’ is ’1’. For example, ’1.2.2’ is the proof step from the second open literal of its parent clause in the proof step named ’1.2’. step_name in Reduction steps refer to the proof step with the clause that contains the literal L2 . clause_number is the number of the used clause in the matrix. term_substitution is of the form bind([vlist ,tlist ]), in which vlist is a list of variables V1 , . . . , Vn and tlist is a list of terms t1 , . . . , tn , such that σ(Vi ) = ti . Example 4. The proof of Pelletier’s problem 24a from Example 1 using the leanTPTP syntax is shown in Figure 5. It is produced by leanCoP 2.2 [14, 11] on the input file in Figure 3 (with simplified variable names and literals L2 of Extension steps moved to the beginning of clauses). 3.3. The Connect++ Syntax Connect++ [6] is a C++ implementation of the connection calculus shown in Figure 1. The proof format of the Connect++ prover uses a stack to represent connection proofs. Each element on the stack corresponds to exactly one proof step in the (formal) connection calculus, and the stack is ordered to represent a depth-first search from the Start rule, exploring the left subtrees of Extensions first. Clauses, and literals within clauses, are numbered from 0. The first element of a proof is start(i), giving the index of the start clause used. Reductions are represented as reduction(p, q) where p denotes the index of the literal L1 in C ∪ {L1 } and q 89 matrix(0, [ -big_p(X), -big_r(X) ]). matrix(1, [ -big_s(X), -big_q(X) ]). matrix(2, [ big_p(a) ]). matrix(3, [ -big_q(X), big_s(X) ]). matrix(4, [ -big_p(X), big_q(X), big_r(X) ]). proof_stack([ start(0), left_branch(0, 2, 0, 2), right_branch(2), left_branch(0, 4, 2, 3), left_branch(0, 2, 0, 4), right_branch(4), left_branch(0, 3, 0, 5), left_branch(0, 1, 0, 6), reduction(0, 1), right_branch(6), right_branch(5), right_branch(3) ]). Figure 6: A proof of Pelletier’s problem 24a using the syntax as returned by Connect++. denotes the index of the element in the path corresponding to L2 . Extensions are represented by left_branch(p, i, j, d) and right_branch(d) where p again denotes the index of the literal L1 in C ∪ {L1 }, i is the index of C2 , j the index of L2 and d the proof tree depth. One aim of the Connect++ syntax is to be quite explicit in stating how the rules of the connection calculus have been applied. This in turn stems from the idea that the simpler a proof checking program is, the more trustworthy it is likely to be, and this simplicity is supported by giving it as much information as possible. In the case of leanCoP, for example, a simplified version might be appropriate because L1 is always the literal at index 0; however this might not be the case, for example, if a prover includes a heuristic for choosing an arbitrary literal with the aim of finding a proof more efficiently. Example 5. The proof of Pelletier’s problem 24a from Example 1 using the Connect++ syntax is shown in Figure 6.5 In this proof, start(0) denotes that clause 0 is used by the Start rule, and left_branch(0,2,0,2) denotes that the first Extension uses the first literal in C ∪ {L1 }, clause 2 and literal 0 within that clause, and is at depth 2 in the tree, and so on. Connect++includes a proof checker. It is a short piece of Prolog code and uses Prolog’s unification to build the substitution. However, it is straightforward to extend Connect++’s syntax to specify explicitly the substitution of the returned connection proof. 4. A Proposed Syntax for Connection Proofs We propose a syntax, which follows more closely the TSTP format described in Section 3.1 and generalizes the leanTPTP format presented in Section 3.2 with the following modifications: • include information about the parent node, which allows the use of arbitrary proof step names in the first argument, • use the rule_info argument of the inference expression to specify clause name of C1 , position of literal L1 in the parent clause, position of literal L2 in C2 (or in the active path), substitution σ applied to C2 and the (instantiated) active Path. 5 Note that the prover produces a slightly different proof of the problem by way of a different choice of C2 in the third Extension. Also, literals are negated throughout the matrix as Connect++ works in the negative (conjunctive normal form) representation, starting with the negation of the stated problem. 90 %----------------------------------------------------- fof(pel24_1, axiom, ~ ?[X]:(big_s(X)&big_q(X)), file(’SYN054a’,pel24_1)). fof(pel24_3a, axiom, ?[X]: big_p(X), file(’SYN054a’,pel24_3a)). fof(pel24_4a, axiom, ![X]:(big_q(X)=>big_s(X)), file(’SYN054a’,pel24_4a)). fof(pel24_2, axiom, ![X]:(big_p(X)=>big_q(X)|big_r(X)), file(’SYN054a’,pel24_2)). fof(pel24, conjecture, ?[X]:(big_p(X) & big_r(X)), file(’SYN054a’,pel24)). cnf(1, plain, [big_p(X), big_r(X)], clausify(pel24)). cnf(2, plain, [big_s(X), big_q(X)], clausify(pel24_1)). cnf(3, plain, [-(big_p(a))], clausify(pel24_3a)). cnf(4, plain, [big_q(X), -(big_s(X))], clausify(pel24_4a)). cnf(5, plain, [big_p(X), -(big_q(X)), -(big_r(X))], clausify(pel24_2)). cnf(6,plain,[big_p(a),big_r(a)],inference(start,[1,bind([X],[a]),path([])],[])). cnf(7,plain,[-(big_p(a))],inference(extension,[3,lit(1,1),path([big_p(a)])],[6])). cnf(8,plain,[big_p(a),-(big_q(a)),-(big_r(a))], inference(extension,[5,lit(2,3),bind([[X],[a]]),path([big_r(a)])],[6])). cnf(9,plain,[-(big_p(a))],inference(extension,[3,lit(1,1),path([big_r(a),big_p(a)])],[8])). cnf(10,plain,[big_s(a),big_q(a)], inference(extension,[2,lit(2,2),bind([[X],[a]]),path([big_r(a),-(big_q(a))])],[8])). cnf(11,plain,[big_q(a),-(big_s(a))], inference(extension,[4,lit(1,2),bind([[X],[a]]),path([big_r(a),-big_q(a)),big_s(a)])],[10])). cnf(12,plain,[-(big_q(a))], inference(reduction,[lit(1,2),path([big_r(a),-(big_q(a)),big_s(a)])],[11])). %----------------------------------------------------- Figure 7: A connection proof of Pelletier’s problem 24a using the proposed syntax. A (clausal) connection proof using the proposed syntax is a list of proof steps of the form cnf(name,plain, formula,inference(rule_name,rule_info,parent)). in which name is the name of the proof step, formula is the used (instantiated) clause C2 (in case of a Start or Extension step) or a list containing L2 (in case of a Reduction step),6 rule_name is one of start, reduction or extension, and parent is a list containing the name of the previous (parent) proof step; furthermore, rule_info is a list of the form [clause_name,lit(lit1,lit2),bind([vlist,tlist]),path(plist)] in which clause_name is the name of the (input) clause C1 , lit1 is the position of the literal L1 in the parent clause (in case of a Reduction or Extension step), lit2 is the position of the literal L2 in the clause C2 (in case of an Extension step) or in the active path (in case of a Reduction step), vlist is a list of variables V1 , ..., Vn in C2 and tlist is a list of terms t1 , ..., tn , such that σ(Vi ) = ti , plist is the list of literals in the active path.7 For the Start step, parent is empty, for Reduction steps, the argument clause_name is omitted. The arguments lit, bind and path can be omitted.8 Example 6. The proof of Pelletier’s problem 24a from Example 1 using the described syntax is shown in Figure 7.9 A simplified proof omitting redundant arguments is shown in Figure 8. 6 Clauses C1 , C2 and literals L1 , L2 refer to the corresponding elements of the connection calculus in Figure 1. 7 In the future, TSTP inference status information might be included. Note the fact that once a proof is found, it is not relevant for its presentation how the (rigid) substitution σ was calculated (for example, by using free variables). 8 These arguments can be re-calculated from the other (given) information or might not be relevant for some users (for example, the order of branches in the proof tree). 9 The presentation of the input clauses (proof steps pel24* and proof steps 1 to 5) follows the standard TPTP syntax. 91 %----------------------------------------------------- cnf(1, plain, [big_p(X), big_r(X)], clausify(pel24)). cnf(2, plain, [big_s(X), big_q(X)], clausify(pel24_1)). cnf(3, plain, [-(big_p(a))], clausify(pel24_3a)). cnf(4, plain, [big_q(X), -(big_s(X))], clausify(pel24_4a)). cnf(5, plain, [big_p(X), -(big_q(X)), -(big_r(X))], clausify(pel24_2)). cnf(6,plain,[big_p(a),big_r(a)],inference(start,[1],[])). cnf(7,plain,[-(big_p(a))],inference(extension,[3],[6])). cnf(8,plain,[big_p(a),-(big_q(a)),-(big_r(a))],inference(extension,[5],[6])). cnf(9,plain,[-(big_p(a))],inference(extension,[3],[8])). cnf(10,plain,[big_s(a),big_q(a)],inference(extension,[2],[8])). cnf(11,plain,[big_q(a),-(big_s(a))],inference(extension,[4],[10])). cnf(12,plain,[-(big_q(a))],inference(reduction,[],[11])). %----------------------------------------------------- Figure 8: A simplified connection proof of Pelletier’s problem 24a using the proposed syntax. 5. Conclusion In this paper, we described the syntax of the connection proofs returned by two existing connection provers for classical first-order logic, and proposed a syntax for a proof format that fulfils the requirements listed in Section 2.1. As mentioned in the introduction, it should not be seen as a final specification, but as a foundation to initiate discussions within the community in order to finalize such a specification taking further proof formats [4, 7, 18, 21] into account. Compared to the (previous) leanTPTP syntax, the proposed syntax follows more closely the TPTP/TSTP syntax, retaining the slightly simpler representation of proofs as connection tableau, while also including additional information, such as the active path. The latter information is useful when proof steps are to be carried out independently, e.g., in parallel, as all necessary information is included in the description of each proof step. Similar to the TPTP/TSTP format, the leanTPTP format and the Connect++ format, the proposed proof format uses Prolog terms to represent connection proofs. This allows the use of simple Prolog code to implement proof checkers as done, for example, in leanCoP and Connect++. A common standard for presentation of derivations and proofs will increase the interoper- ability between ATP systems, ATP tools, and application software. For example, Connect++ includes a tool to translate connection proofs into a LaTeX output of the formal calculus. A standardized syntax would make it possible to use this tool in combination with other connec- tion provers. Such a standard would also allow the development of tools to translate connection proofs into sequent proofs [5], which are often used in interactive proof editors, such as Coq [1], NuPRL [3] or PVS [16]. To this end, a standardized syntax for sequent proofs would be desirable as well. A possible extension of the current work includes the specification of a syntax to represent non-clausal connection proofs [12] or connection proofs in non-classical logics [10, 13]. These extensions should be kept in mind already when developing a format for clausal connection proofs in classical logics. For example, the connection calculi for intuitionistic and modal logic use an additional prefix substitution, which could be just added to the rule_info argument. Furthermore, future work include the specification of proof formats for other popular proof calculi, such as sequent calculi or (standard) tableau calculi. 92 References [1] Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development - Coq’Art. Texts in Theoretical Computer Science. Springer-Verlag, 2004. [2] W. Bibel. Automated Theorem Proving. Vieweg and Sohn, 1987. [3] R. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986. [4] M. Färber, C. Kaliszyk, and J. Urban. Machine Learning Guidance and Proof Certification for Connection Tableaux. arXiv:1805.03107v3 [cs.LO], 2018. [5] G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 36:176–210, 405–431, 1935. [6] S. B. Holden. Connect++: A New Automated Theorem Prover Based on the Connection Calculus. In J. Otten and W. Bibel, editors, Workshop on Automated Reasoning with Connection Calculi (AReCCa), CEUR Workshop Proceedings. CEUR-WS.org, 2023. [7] C. Kaliszyk, J. Urban, and J. Vyskočil. Certified Connection Tableaux Proofs for HOL Light and TPTP. In Certified Programs and Proofs (CPP), pages 59–66, ACM, 2015. [8] R. Letz and G. Stenz. Model Elimination and Connection Tableau Procedures. In A. Robin- son and A. Voronkov, editors, Handbook of Automated Reasoning, pages 2015–2114. Elsevier Science, 2001. [9] D.W. Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the ACM, 15(2):236–251, 1968. [10] J. Otten. Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic. In B. Beckert, editor, TABLEAUX 2005, LNAI, volume 3702, pages 245–261. Springer, 2005. [11] J. Otten. Restricting Backtracking in Connection Calculi. AI Communications, 23(2-3):159– 182, 2010. [12] J. Otten. A Non-clausal Connection Calculus. In K. Brünnler, G. Metcalfe, editors, TABLEAUX 2011, LNAI, volume 6793, pages 226–241. Springer, 2011. [13] J. Otten. MleanCoP: A Connection Prover for First-Order Modal Logic. In S. Demri, D. Kapur, C. Weidenbach, editors, IJCAR 2014, LNAI, volume 8562, pages 269–276. Springer, 2014. [14] J. Otten and W. Bibel. leanCoP: Lean Connection-Based Theorem Proving. Journal of Symbolic Computation, 36(1-2):139–161, 2003. [15] J. Otten and G. Sutcliffe. Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi. In B. Konev, R.A. Schmidt, S. Schulz, editors, PAAR 2010, EPiC, volume 9, pages 95–105. EasyChair, 2010. [16] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas. PVS: Combining Specification, Proof Checking, and Model Checking. In R. Alur and T.A. Henzinger, editors, Computer- Aided Verification, LNCS, volume 1102, pages 411–414. Springer, 1996. [17] F.J. Pelletier. Seventy-five Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning, 2(2):191–216, 1986. 93 [18] G. Reis. Importing SMT and connection proofs as expansion trees. Electronic Proceedings in Theoretical Computer Science, 186:3–10, 2015. [19] G. Sutcliffe. The TPTP problem library and associated infrastructure. Journal of Automated Reasoning, 59(4):483–502, 2017. [20] G. Sutcliffe, S. Schulz, K. Claessen, and A. Van Gelder. Using the TPTP Language for Writing Derivations and Finite Interpretations. In U. Furbach and N. Shankar, editors, IJCAR 2006, LNAI, volume 4130, pages 67–81. Springer, 2006. [21] A. Wolf and J. Schumann. ILF-SETHEO. In W. McCune, editor, CADE-14, LNCS, volume 1249, pages 61–64. Springer, 1997. 94