Abduction Prover in Isabelle/HOL YUTAKA NAGASHIMA, Institute of Computer Science, the Czech Academy of Sciences, Czechia DANIEL SEBASTIAN GOC
arXiv:2606.04877v1 [cs.LO] 3 Jun 2026
Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assistants. We address this problem by introducing the Abduction Prover for Isabelle/HOL. Given a challenging proof goal, the Abduction Prover constructs a proof script for the goal by identifying useful conjectures using abductive reasoning.
1
Introduction
Consider the following proof goal presented in a Haskell-like syntax. data List 𝛼 = [ ] | 𝛼 : (List 𝛼) + :: List 𝛼 => List 𝛼 => List 𝛼 + [ ] 𝑦𝑠 = 𝑦𝑠 + (𝑥:𝑥𝑠) 𝑦𝑠 = 𝑥:(𝑥𝑠 + 𝑦𝑠) rev1 :: List 𝛼 => List 𝛼 => List 𝛼 rev1 [ ] ys = ys rev1 (x:xs) ys = rev1 xs (x:ys) rev2 :: List 𝛼 => List 𝛼 rev2 [ ] = [ ] rev2 (𝑥:𝑥𝑠) = (rev2 𝑥𝑠) + (𝑥:[ ]) theorem revs_eq: "rev1 𝑥𝑠 [ ] = rev2 𝑥𝑠" This theorem, named revs_eq, states the equivalence of two reverse functions, rev1 and rev2, defined on lists of arbitrary types in Isabelle/HOL’s underlying logic: classical higher-order logic on simply typed lambda calculus. Conventionally, Isabelle users apply tools called proof tactics to transform proof goals to develop proof scripts. Proof tactics are meta-programming tools that transform proof goals at hands into shapes closer to the obviously correct statement True. Isabelle offers more than 200 tactics, and it is users’ responsibility to keep applying appropriate tactics to proof goals until they become obviously true. This approach is called tactical theorem proving, and this is the dominant style adopted by the major interactive theorem provers (ITPs) such as Rocq [6], Lean [1], and the HOL prover [5]. For example, the first step to prove this goal is to apply the induction tactic as follows: theorem revs_eq: "rev1 𝑥𝑠 [] = rev2 𝑥𝑠" apply (induct 𝑥𝑠) This leads to two new sub-goals, corresponding to the base case and the step case of the structural induction on the variable xs. subg1. rev1 [] [] = rev2 [] subg2. rev1 𝑥𝑠 [] = rev2 xs =⇒ rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠) The second sub-goal itself is a significant challenge. Further applications of tactics to the second sub-goal may complicate it. Addressing it effectively requires first conjecturing several auxiliary lemmas and proving them. Generally, when using ITPs, we have to address the following question: Q1: What tactics should we apply with which arguments? Authors’ Contact Information: Yutaka Nagashima, Institute of Computer Science, the Czech Academy of Sciences, Prague, Czechia; Daniel Sebastian Goc.
2
Nagashima et al.
Fig. 1. Proof script produced by the AbductionProver for the running example.
Q2: When should we stop applying tactics and introduce auxiliary lemmas? Q3: What auxiliary lemmas should we introduce? To automatically address these three questions, this paper presents the AbductionProver. Given a challenging proof goal, the AbductionProver keeps generating and proving useful auxiliary lemmas to prove the challenging goal. For example, in our running case, it produces the proof script shown in Fig. 1.
Abduction Prover in Isabelle/HOL
revs_eq. rev1 𝑥𝑠 [] = rev2 𝑥𝑠
3
induct []
revs_eq. rev1 𝑥𝑠 [] = rev2 𝑥𝑠 uct ind induct 𝑥𝑠
subg1’. rev1 𝑥𝑠 [] = rev2 [] subg1. rev1 [] [] = rev2 [] subg2’. rev1 𝑥𝑠 [] = 𝑥2 =⇒ subg2. rev1 𝑥𝑠 [] = rev2 𝑥𝑠 =⇒ rev1 𝑥𝑠 [] = 𝑥1:𝑥2 rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠) Fig. 2. The default computational model of Isabelle: Tactical theorem proving as an implicit OR-tree traversal.
Our implementation is specific to Isabelle/HOL; however, the underlying concepts presented in this paper are transferrable to other tactical theorem provers with similar ecosystems. In the rest of the paper, we introduce the AbductionProver in a step-by-step manner. That is, we start by presenting the default manual proof search model of Isabelle against a simpler problem in Section 1. And gradually add components of the AbductionProver in each section to overcome each challenge. The key to this reasoning is the two flags attached to nodes, completion status flag and contributivity status flag, and the distinction between two kinds of graphs: the abduction graph and the solution graph. Contrary to other applications of artificial intelligence in theorem proving, the AbductionProver currently does not directly rely on machine learning or meta-heuristic approaches such as evolutionary computation. Instead, it embodies a proof search framework, which could benefit from such approaches. Although this paper primarily focuses on the design and architecture of the AbductionProver, a working implementation has been developed on top of the PSL framework for Isabelle/HOL. To facilitate reproducibility, future experimentation, and further extensions, the following public artifacts related to this work are available online: • Demonstration video: https://www.youtube.com/watch?v=rXU-lJxP_GI • PSL framework for Isabelle/HOL: https://github.com/data61/PSL 2 2.1
From Implicit OR-tree Exploration To AND-OR graph Expansion Tactic-Based Proof Search as Implicit OR-tree Exploration
We start by reviewing the process of tactical theorem proving as an implicit OR-tree exploration using our running example from Section 1. Fig. 2 shows three scenarios of applying induction. The left scenario passes the empty list as the argument to the induct tactic, the one in the middle applies structural induction on the 𝑥𝑠 on right-hand side, and the right one applies structural induction on both occurrences of 𝑥𝑠. Fig. 2 also exhibits a few notable issues that are important to understand the design of the AbductionProver later in this paper. First, this figure represents the tactical theorem proving as an implicit OR-tree traversal, which is the default computational model of Isabelle. In this mode, multiple subgoals emerging from the previous step are grouped into one node. Second, the left scenario did not make meaningful progress: the resulting subgoal is the same as the original goal. Therefore, the choice of tactic argument is inappropriate. Nevertheless, this subgoal is still logically provable, posing a challenge in avoiding exponential blow-up of the search space. We will discuss how the AbductionProver handles such cases in Section 6.3. Third, we can consider the tactic applications in the middle and on the right as instances of Modus Ponens (MP) with multiple premises. For example, the application of the induct tactic
4
Nagashima et al.
ensures that if we prove the base-case and step-case, that is tantamount to proving the original goal: (induct xs) subg1 ∧ subg2 =⇒ revs_eq subg1 ∧ subg2 MP revs_eq Generally, tactic applications can be seen as following using Modus Ponens: tactic sub-goals =⇒ goal sub-goals MP-tac goal The directions of the arrows differ between the figure and the derivation trees, and this requires explanation. In the derivation trees, =⇒ represents logical implication: sub-goals =⇒ goal means that we must prove the goal assuming the sub-goals. In contrast, the arrows connecting nodes in Fig. 2 indicate the direction of tree traversal, which is the standard notation for tree search. Therefore, goal −→ sub-goal denotes that we proceed to sub-goal to prove goal . For problems at this difficulty level, we can often identify provably correct arguments for the induct tactic by executing a backtracking search over tactic combinations and argument candidates. The backtracking search aligns well with the OR-tree traversal model shown in Fig. 2, as it obtains final proof scripts by concatenating the labels on the edges from the root node to the leaf node representing proof completion [2]. This approach effectively addressed Q1 in Section 1, and we use it in our tool as explained in Section 4.2. However, its efficacy was limited to simple problems that did not require explicit conjecturing. 2.2
Tactic-Based Search as the Construction of an AND-OR Tree
Another way to understand such computation is by considering it as an expansion of an AND-OR tree, as illustrated in Fig. 3. When depicting AND-OR structures in this paper, we use double-line borders for AND-nodes within AND-OR models to indicate that all their sub-structures must be proved. In contrast, single-line borders represent OR-nodes to signify that only one of their sub-structures needs to be proven. Such AND-OR trees might seem more intuitive to many ITP users, as they view each subgoal as an individual problem. However, the AND-OR tree model makes it challenging to keep track of which sub-trees need to be proved, especially after applying multiple tactics in sequence, causing the tree to grow deeper. Also, this model deviates from the internal representation of proof goals in Isabelle and Lean, which are closer to the OR-tree representation, making it less suitable as the platform to execute the aforementioned backtracking search over tactic applications. The AbductionProver combines the strengths of both representations, by performing a smallscale backtracking search over the OR-tree model while orchestrating large-scale proof automation using a data-structure inspired by the AND-OR tree model, as explained in Section 4. 2.3
One-Step Conjecturing
Section 1 demonstrated that, we often need to first establish intermediate lemmas as stepping stones to prove challenging theorems. Such intermediate lemmas have to satisfy the following conditions: C1: The lemmas must be useful for proving the challenging theorems. C2: The lemmas must themselves be provable. C3: The lemmas must be easier to prove than the challenging theorems. For example, we can prove our running example with the following lemma.
Abduction Prover in Isabelle/HOL
5
induct []
revs_eq
revs_eq
.. .
revs_eq
subg1’ ∧ subg2’ subg1’
subg2’
... induct 𝑥𝑠 simp only: subg1 simp only: subg2 subg1 ∧ subg2 subg1
subg2
Fig. 3. Tactic application as an AND-OR tree construction.
helper: "rev1 𝑥𝑠 𝑦𝑠 = rev2 𝑥𝑠 + 𝑦𝑠" sorry subg2: "rev1 𝑥𝑠 [] = rev2 xs =⇒ rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠)" apply(auto intro: helper) done where we naively assumed the correctness of the helper lemma using the sorry keyword. Note that this paper’s main focus is on our approach to identify useful lemmas out of many candidate conjectures, and we defer the description of conjecture generation to Section 5, in contrast to other projects that focus on producing such auxiliary lemmas using machine learning techniques. Similarly to the application of the induct tactic in Section 2.1, we consider this proof as an instance of Modus Ponens as follows: helper =⇒ subg2
(auto intro: helper) subg2
helper
sorry MP
Based on this interpretation, this paper uses abductive reasoning to identify useful lemmas for many challenging theorems. The key is to produce many candidate conjectures and filter less promising candidates using proof automation tools and counterexample finders. Consider the following three candidate conjectures, ⊥, conj, and ⊤, as follows: conj =⇒ subg2 conj ⊤ =⇒ subg2 ⊤ ⊥ =⇒ subg2 ⊥ MP-conj subg2 subg2 subg2 where ⊥ stands for False and ⊤ stands for True in the underlying non-minimal logic that admits the law of explosion. The left derivation tree represents an extreme case where the candidate conjecture is a simple False statement. In this derivation tree, the left branch (⊥ =⇒ subg2) can be easily proven because the underlying logic supports the law of explosion. However, it is impossible to prove the right branch (⊥). Generally, assuming False conjectures allows us to prove challenging goals, but such conjectures themselves cannot be proven. The derivation tree on the right illustrates the opposite extreme, where the candidate conjecture is a simple True statement. In this tree, the right branch trivially holds, but proving the left branch is no easier than proving the original goal. This is because having True as an assumption provides no additional advantage in proving subg2. The conjectures we aim for must not be equivalent to False and should also be useful for proving the final goals. To identify such conjectures, Nagashima et al. first apply Isabelle’s proof tactic fastforce to filter in candidate conjectures that are provably useful to attack the final goals. Subsequently, they apply counterexample finders (Quickcheck and Nitpick) to filter out conjectures that are equivalent to False. This process generates conjectures that are provably useful but not demonstrably equivalent to False. However, it does not guarantee that the final criterion for intermediate lemmas — C3 ease
6
Nagashima et al.
le rexamp counte
⊥
for ⊥
subg2
difficul t
auto intro: helper ⊤ =⇒
to prov e subg2
⊤
helper Fig. 4. Tactic application as an OR-tree construction.
of proof — is satisfied. Only when we successfully prove the lemma using smaller computational resources can we confirm that the lemmas meet all three criteria. Similar to the case with tactics, this process can be viewed either as an OR-tree search, as illustrated in Fig. 4. In this figure, two dashed gray edges extend from subg2 to dashed gray nodes: ⊥ and ⊤ , indicating that the abductive reasoning process decided not to pursue these branches, with the reasons provided as the edge labels. Based on this intuition, Nagashima et al. automated abductive reasoning as a backtracking search over an implicit OR-tree to identify useful conjectures. They demonstrated the efficacy of this approach with a small example; however, its computational complexity increases rapidly when applied to challenging problems that require nested conjecturing. Not only does the search space grow exponentially with the depth of the implicit OR-tree, but the same conjectures are also produced in different branches, causing duplication. For instance, a common property, such as the associativity of the + operator in this example, can be useful for proving many conjectures appearing in different branches. This results in repeated production of this lemma and its proofs, which we address in Section 2.5. 2.4
Tactic Application as Implicit Conjecturing
Attentive readers may have noticed the similarities between MP-tac and MP-conj, as well as between Fig. 2 and Fig. 4. That is, both tactic applications and explicit conjecturing are instances of Modus Ponens. Since they are based on the same rule, the AbductionProver sees tactic application as implicit conjecturing and treats them in essentially the same way with adjustments detailed in Section 4.3. That is, instead of having separate trees for each proof goal appearing during large proof developments, we have one AND-OR tree that encompasses both tactic applications and conjecturing in a monolithic manner as shown in Fig. 5. This way, the AbductionProver simplifies the question of when to introduce new lemmas, presented as Q2 in Section 2, into the straightforward task of deciding which node to expand next within a single structure, the Abduction Graph. Although this may resemble the standard best-first search problem found in many other domains, there is a key difference: the goal of expanding nodes is to grow the AND-OR structure until it encompasses a sub-structure that represents a complete proof of the root node. 2.5
From AND-OR Tree to AND-OR Graph
As discussed in Section 2.2, the AND-OR tree model makes it challenging to keep track of which subtrees need to be proved compared to the OR-tree model, which represents a proof script as a single path from the root node to a leaf node, signifying the completion of the proof. Furthermore, the OR-tree model frames proof search as a procedure to identify a single leaf node, making it more aligned not only with Isabelle’s default computation model but also with common AI problems in other fields.
Abduction Prover in Isabelle/HOL
induct
... ...
...
7
Nil
revs_eq induct 𝑥𝑠 simp only: subg1 simp only: subg2 subg1 ∧ subg2
subg1
difficu le subg2 lt to p xamp e r e rove t coun ⊤ =⇒ auto intro:helper ⊥ s r u bg2 fo ⊥ helper
⊤
helper Fig. 5. Tactic application and explicit conjecturing as an AND-OR tree construction.
Despite these considerations, the AbductionProver is based on an AND-OR model because different intermediate goals often require the same conjectures as their stepping stones. For instance, the associativity of the + operator is likely to be useful for solving many intermediate goals encountered while trying to prove revs_eq. To avoid duplicated lemmas, we further switched from the AND-OR tree model to an AND-OR graph model, since the graph model better represents situations where multiple sub-goals can be proved using the same intermediate lemmas. Fig. 6 illustrates multiple dependencies on a single lemma using the running example. Specifically, this figure shows that revs_eq can be directly proved by applying the metis tactic once helper is established. The metis tactic takes three arguments: helper, rev1.simps, and rev2.elims. The first argument (helper) appears in the graph as helper and helper . On the contrary, rev1.simps and rev2.elims are absent from the graph; they are registered in the background proof context when the relevant functions (rev1 and rev2) are defined. These lemmas are made available as contextual information for tools like sledgehammer. Overall, the AbductionProver uses the proof context in a restrictive manner: it tries to register as few additional lemmas as possible in the background context so that it can explicitly handle the inter-dependencies among auxiliary lemmas. Having introduced the benefits of using the AND-OR graph model for proof search involving multi-step conjecturing, we now invite readers to reflect on the following question: Must such AND-OR graphs be acyclic, or can they be cyclic? 3
Reasoning Over Abduction Graph
Before answering this question, we examine how to reason over abduction graphs. The two major questions to address when using abduction graphs are as follows: (1) Completion: Which nodes have already been proved? (2) Contributivity: Which nodes should still be attempted to prove? As noted in Section 2.5, tracking which nodes have already been proved is challenging with ANDOR trees and even more so with AND-OR graphs. Therefore, we first determine how to verify whether revs_eq is completely proved in our running example.
8
Nagashima et al.
revs_eq
met
induct 𝑥𝑠 simp only: subg1 simp only: subg2 subg1 ∧ subg2 subg1
subg2
is hel pe rev r re v1 2.e lim .sim ps s
auto intro:helper
helper helper
Fig. 6. Tactic application and conjecturing as an AND-OR graph construction.
revs_eq
revs_eq
subg1 ∧ subg2
subg1 ∧ subg2 ① subg1 ✓
subg1
subg2
subg2 ② ①
helper
Fig. 7. Upward completion check due to subg1.
helper
helper ✓
helper
3.1
③
②
Fig. 8. Upward completion check due to helper.
Completed Nodes: Which Nodes Are Already Proved?
At the stage shown in Fig. 6, none of the OR-nodes have been proved yet, including the root node ( revs_eq ). For the root node, the graph only indicates that proving either subg1 ∧ subg2 or helper would be equivalent to proving revs_eq . However, neither of these and-nodes have been proved. Fig. 7 and Fig. 8 illustrate how this situation changes when subg1 and helper are proved, respectively. The specific steps taken to prove these or-nodes are not the focus; rather, we examine how proving them affects the proof completion status of their ancestral nodes at this stage. In Fig.7, even though we prove subg1 , this does not immediately affect other nodes, since the only parent AND-node ( subg1 ∧ subg2 ) still has an unproved sub-goal ( subg2 ). The dashed arrow from subg1 to subg1 ∧ subg2 indicates that the proof of the subg1 fails to update the proof status of subg1 ∧ subg2 . As indicated by this arrow, the process works primarily in a bottom-up manner. However, when evaluating the proof completion status of an ancestral ANDnode such as subg1 ∧ subg2 , it must look downward exactly one layer to gather the proof statuses of all its immediate child OR-nodes ( subg1 and subg2 ). To facilitate this, the graph must maintain the current proof completion status of each OR-node. Fig. 8, on the other hand, shows how completion check propagates when we prove helper without proving subg1 . In this scenario, proving helper automatically proves its parental ANDnode ( helper ), because helper is the only child of helper . And this in turn is tantamount
Abduction Prover in Isabelle/HOL
9
to prove revs_eq and subg2 . However, subg2 does not change the status of subg1 ∧ subg2 , since subg1 is not proved. These figures demonstrated how to determine whether branch nodes are considered proved, assuming leaf OR-nodes are proved. While we defer the discussion of proving leaf nodes to Section 4.2, we now introduce the notions of completed nodes and atomic proofs to distinguish the efforts required to prove branch nodes and leaf nodes. In general, a leaf node is said to have an atomic proof script if its proof does not rely on other nodes in the graph, whereas a branch node is considered completed if the graph contains enough labeled edges and atomically proved leaf nodes to establish its proof. On the contrary, if a node is not completed, the node is said to be uncompleted. Specifically, an OR-node in an abduction graph is completed if it satisfies one of the following conditions: D1: The OR-node has an atomic proof. D2: The OR-node points to at least one AND-node that is completed. In contrast, an AND-node in an abduction graph is completed if it satisfies the following condition: E1: The AND-node points to OR-nodes, all of which are completed. In Fig. 8, for example, subg1 ∧ subg2 remains uncompleted, since it has an uncompleted child OR-node ( subg1 ). However, should we still complete subg1 for subg1 ∧ subg2 after proving helper ? 3.2
Contributive Nodes: Which Nodes Are Still Worth Proving?
To determine whether a node should still be completed, we need to know if it can still contribute to our objective: completing the root node. From this perspective, Fig. 9 and Fig. 10 check if we should complete subg1 and subg1 ∧ subg2 after proving helper . First, Fig. 9 highlights in blue the nodes that are considered completed after proving helper in Fig. 8. Then, Fig. 10 marks the nodes that remain uncompleted but are no longer necessary for achieving our goal with dashed boundaries. That is, following the direction of arrows from the root node: Since the root node is already completed, there is no need to complete its child node, subg1 ∧ subg2 , even though it has not been proved yet, as illustrated by the edge labeled with ①. This process propagates downwards: Since subg1 ∧ subg2 is no longer necessary, there is no 2 need to prove its child node, subg1 either, as shown by the edge labeled with ○. In this particular case, it was straightforward to determine the unworthiness of these two nodes, since both nodes ( subg1 ∧ subg2 and subg1 ) are pointed by only one parental node. However, if multiple OR-nodes point to one AND-node, completing one of the parent OR-nodes does not always eliminate the need to complete the AND-node. Fig. 11 and Fig. 12 illustrate this situation using an alternative auxiliary lemma, repleh, to prove subg2. First, Fig. 11 shows that proving the OR-node repleh is sufficient to complete repleh and subg2 . This is why these three nodes are highlighted in blue in Fig. 12. However, this does not eliminate the need for helper in Fig. 12, because helper is pointed to by revs_eq , and revs_eq itself still needs to be completed. Then, since the necessity for helper has not changed this time, there is no need to check the necessity for its child node, helper . Generally, a node is considered non-contributive if its completion does not contribute to the completion of the root node. On the contrary, if its completion does contribute to the completion of the root node, the node is said to be contributive.
10
Nagashima et al.
revs_eq revs_eq
① subg1 ∧ subg2
subg1 ∧ subg2
② subg1
subg1
subg2
subg2 helper helper helper ✓
Fig. 9. After completion check due to helper.
helper ✓ Fig. 10. Downward contributivity check from the root. subg1 ∧ subg2 and subg1 are no longer contributive.
Specifically, an OR-node becomes non-contributive when it satisfies at least one of the following conditions: F1: The OR-node is already completed. F2: Both of the following two conditions hold: • The OR-node is not the root node. • The OR-node is not pointed to by any contributive AND-node. In contrast, an AND-node becomes non-contributive when it satisfies at least one of the following conditions: G1: The AND-node is already completed. G2: The AND-node is not pointed to by any contributive OR-node. Following De Morgan’s laws, an OR-node becomes contributive when it satisfies both of the following conditions: H1: The OR-node is still uncompleted. H2: At least one of the following two conditions holds: • The OR-node is the root node. • The OR-node is pointed to by at least one contributive AND-node. In contrast, an AND-node becomes contributive when it satisfies both of the following condition: I1: The AND-node is still uncompleted. I2: The AND-node is pointed to by at least one contributive OR-node. 3.3
Upwards Completion Check Before Downwards Contributivity Check.
The conditions presented in Sections 3.1 and 3.2 imply that updating a node requires knowledge of the current status of its neighboring nodes. For this reason, we must store the status of contributive nodes as required by the update process. Regarding the dependencies among nodes in maintaining up-to-date status information, the criteria from these sections indicate the following: (1) A node’s completion status depends on the completion status of its child nodes. (2) A node’s completion status is independent of the contributivity status of any node. (3) A node’s contributivity status depends on the contributivity status of its parent nodes. (4) A node’s contributivity status depends on its own completion status.
Abduction Prover in Isabelle/HOL
11
revs_eq revs_eq subg1 ∧ subg2 subg1 ∧ subg2 subg1
subg1
③
subg2
subg2
①
② repleh
helper
① repleh ✓
helper
Fig. 11. Upward completion check due to repleh.
repleh
helper
repleh ✓
helper
Fig. 12. Downward contributivity check from the root. helper is still contributive.
revs_eq subg1 ∧ subg2 subg1 epleh subg2 ntro:r auto i auto simp repleh :repleh repleh
auto simp
auto i
ntro:h elper
:helper
helper helper
Fig. 13. Cyclic abduction graph.
From these, we derive the following design principles for the AbductionProver: (1) Completion status changes must be propagated upwards to its ancestors. (2) Propagation of contributivity status changes does not affect completion statuses. (3) Contributivity status changes must be propagated downwards to its descendants. (4) Updates to completion statuses should be finalized before updating contributivity statuses. Now that we know status updates propagate upward for completion status and downward for contributivity status, does this imply that circular dependencies must be disallowed in abduction graphs to prevent infinite loops? 3.4
Cyclic Abduction Graph and Acyclic Solution Graph
Fig.13 is an example abduction graph for our running example, which shows a cyclic dependency between helper and repleh . Specifically, Fig. 13 contains two additional labeled edges compared to Fig. 11. Note the following two key differences from Fig. 9. First, unlike Fig. 11, Fig. 13 assumes that neither helper nor repleh has been proved yet. Second, Fig. 13 has two additional edges, which makes the graph cyclic. We added the edge from helper to repleh , because if we assume repleh we can prove helper as follows:
12
Nagashima et al.
revs_eq
revs_eq
subg1 ∧ subg2 subg1
③
repleh
②
subg2 ②
subg1 ∧ subg2 subg1
subg2
helper
repleh
helper
③ ① repleh ② helper ✓
repleh
helper ✓
Fig. 14. helper newly proved.
Fig. 15. Solution graph in Fig. 14.
repleh: "rev2 𝑥𝑠 + 𝑦𝑠 = rev1 𝑥𝑠 𝑦𝑠" sorry helper: "rev1 𝑥𝑠 𝑦𝑠 = rev2 𝑥𝑠 + 𝑦𝑠" apply (auto simp:repleh) done whereas we added the edge from repleh to helper , because if we assume helper we can prove repleh as follows: helper: "rev1 𝑥𝑠 𝑦𝑠 = rev2 𝑥𝑠 + 𝑦𝑠" sorry repleh: "rev2 𝑥𝑠 + 𝑦𝑠 = rev1 𝑥𝑠 𝑦𝑠" apply (auto simp:helper) done Both proofs are logically valid under the respective assumptions axiomatically introduced by the sorry keyword. Now, we examine how to reason over this cyclic graph by considering the completion update for two cases. Status Updates After Proving helper. Fig. 14 shows the case where we find an atomic proof for helper . The atomic proof for helper makes this leaf OR-node completed. Since helper is the only child of helper , helper also becomes completed (①). Then, since helper is pointed to by three parental OR-nodes rev_eq , subg2 , and, repleh ), all of them become completed (②). While we could stop the status update since the root node has been completed, let us examine how the update propagates from other newly updated OR-nodes ( subg2 and repleh ). subg2 is pointed to by an OR-node ( subg1 ∧ subg2 ), but the other subgoal of subg1 ∧ subg2 is not completed yet. The dashed arrow labeled with ③ fails to complete subg1 ∧ subg2 , since subg1 is uncompleted. On the other hand, the completion of repleh completes its only parent AND-node ( repleh ), since repleh is the only child of repleh , as depicted with the blue arrow labeled with ③. However, the upward propagation stops here, since both parents of repleh are already completed either by the atomic proof for helper or by the propagation labeled with ② for subg2 . Since we completed the root node, we have a minimal subgraph sufficient to prove the root node, which is highlighted in Fig. 15. Notice that even though we completed repleh , repleh , and subg2 , these nodes are not necessary to construct a proof of revs_eq and are not highlighted in Fig. 15 for this reason. Status Updates After Proving repleh. Fig. 16 on the other hand shows the case where we find an atomic proof for repleh . The atomic proof for repleh makes this leaf OR-node completed. Since repleh is the only child of repleh , repleh also becomes completed (①). Then, since repleh is pointed to by two parental OR-nodes ( subg2 and helper ), both of them become completed (②).
Abduction Prover in Isabelle/HOL
13
revs_eq subg1 ∧ subg2 subg1
③
revs_eq ④
subg2
subg1 ∧ subg2 subg1
subg2
② repleh
helper
repleh
helper
① ③ repleh ② helper ✓
repleh ✓
helper
Fig. 16. repleh newly proved.
Algorithm 1 recursive abduction 1: 𝑔𝑟𝑎𝑝ℎ ← set_root 𝑔𝑜𝑎𝑙 2: 𝑐𝑡𝑟 ← 1 3: while 𝑐𝑡𝑟 ≤ limit ∧ ¬proved 𝑔𝑟𝑎𝑝ℎ do 4: 𝑐𝑡𝑟 ← 𝑐𝑡𝑟 + 1 5: 𝑛𝑜𝑑𝑒𝑠 ← get-contributive-leaves 𝑔𝑟𝑎𝑝ℎ 6: fold work-on-node 𝑛𝑜𝑑𝑒𝑠 𝑔𝑟𝑎𝑝ℎ 7: end while 8: show 𝑔𝑟𝑎𝑝ℎ
Fig. 17. Solution graph in Fig. 16.
Algorithm 2 work-on-node 1: 𝑛𝑜𝑑𝑒 ← try-to-prove 𝑛𝑜𝑑𝑒 2: if is-not-proved 𝑛𝑜𝑑𝑒 then 3: 𝑔𝑟𝑎𝑝ℎ ← exp-tactic 𝑛𝑜𝑑𝑒 𝑔𝑟𝑎𝑝ℎ 4: 𝑔𝑟𝑎𝑝ℎ ← exp-template 𝑛𝑜𝑑𝑒 𝑔𝑟𝑎𝑝ℎ 5: 𝑔𝑟𝑎𝑝ℎ ← exp-mutation 𝑛𝑜𝑑𝑒 𝑔𝑟𝑎𝑝ℎ 6: end if 7: 𝑔𝑟𝑎𝑝ℎ ← update-is-completed 𝑛𝑜𝑑𝑒 𝑔𝑟𝑎𝑝ℎ 8: 𝑔𝑟𝑎𝑝ℎ ← update-is-contributive 𝑛𝑜𝑑𝑒 9: return graph
subg2 is pointed to by an OR-node ( subg1 ∧ subg2 ), but the other subgoal of subg1 ∧ subg2 is uncompleted. So, the dashed arrow labeled with ③ fails to complete subg1 ∧ subg2 ). On the other hand, helper is the only child of helper . So, the completion of helper completes helper (③). helper itself is pointed to by two AND-nodes ( subg2 and revs_eq ). While the upward propagation stops at subg2 towards this direction, since subg2 is already completed by ② from repleh , the completion of helper completes the other parent node ( revs_eq ) through ④. Since revs_eq is the root node, we now have a minimal subgraph sufficient to prove the root node, which is highlighted in Fig. 17. Notice that even though we completed subg2 , this node is not necessary to construct a proof of revs_eq and is not highlighted in Fig. 17. Acyclic Solution Graphs. These examples have demonstrably answered the question raised in Section 2.5: Must our AND-OR graphs be acyclic, or can they be cyclic? Yes, abduction graphs can be cyclic to represent mutual dependencies among intermediate lemmas. However, when completing the root node, the abduction graph must contain a subgraph sufficient to prove the root node, and that subgraph must be acyclic to avoid circular arguments. We refer to such a minimal acyclic subgraph as a solution graph. 4
System Description A: Recursive Abduction as the Expansion of Abduction Graph
14
Nagashima et al.
Algorithm 3 try-to-prove 1: Ors [ 2: Thens [ Auto, IsSolved ], 3: Thens [ 4: SmartInduct, 5: Ors [ 6: 7: 8: 9: 10: 11: ]
Thens [ SimpAll, IsSolved ], Thens [ Auto, IsSolved ] ] ] Thens [ Hammer, IsSolved ]
Algorithm 4 exp-tactic 1: Alts [ 2: Clarsimp, 3: Thens [ 4: SmartInduct, 5: 6: 7: ]
Alts [ SimpAll, Auto ] ]
Section 3 introduced the reasoning process over abduction graphs. Now, we present the algorithm for building abduction graphs to search for proof scripts. First, we describe the general workflow as Algorithm 1 and 2, deferring the concrete definitions of certain functions to Section 4.2 and 4.3. 4.1
The Main Loop for Recursive Abduction.
The AbductionProver’s overall flow is characterized by its ability to expand the abduction graph recursively by producing contributive conjectures. This recursive nature is realized by the while rule in Algorithm 1. Algorithm 1 first initializes the graph with the root OR-node, representing the final goal provided by users, in Line 1. Then, it sets the counter (ctr) to 1. In the main while loop, Algorithm 1 increments the counter (Line 4) and fetches a subset of OR-leaf nodes that are still needed to prove the root node (Line 5). Then, it applies work-on-node to for each such OR-node (Line 6). In Algorithm 2, work-on-node first attempts to find an atomic proof for the given OR-leaf node, using try-to-prove, which we discuss in Section 4.2 (Line 1). Then, if try-to-prove fails to find an atomic proof for the OR-leaf node, Algorithm 2 expands the abduction graph for this node by applying tactics (Line 3), generating conjectures using predefined templates (Line 4), or employing mutation algorithms (Line 5). Regardless of whether work-on-node successfully proves the OR-node or expands the graph for it, the algorithm updates the graph based on the following information: the proof status of the OR-node and the addition of new edges and nodes from one of the exp- functions. This update is performed using the procedures discussed in Section 3.1 and Section 3.2 (Lines 7–8). Algorithm 1 exits the main while loop when the counter reaches a certain threshold or when the root node is completed. Now we look more closely to the concrete functions, try-to-prove, exp-tactic, exp-template, and exp-mutation. Notably, the first two functions internally utilize the OR-tree model introduced in Section 2.1. Since their primary focus is on specific OR-nodes rather than the dependencies within the overall abduction graph, we leverage the simplicity of the OR-tree model to employ the PSL [2] framework for small-scale automation. 4.2
try-to-prove: Attempt to Find Atomic Proofs For OR-leaf Nodes.
To build a solution graph within an abduction graph, one has to find atomic proofs for certain OR-leaf nodes. To achieve this, we employ a proof strategy in PSL [2], as outlined in Algorithm 3.
Abduction Prover in Isabelle/HOL
15
revs_eq. rev1 𝑥𝑠 [] = rev2 𝑥𝑠 7. t 12. s in o c t u ledg u a du 1. d eham n c i t mer 2. 𝑥𝑠 error subg1’∧subg2’ subg1∧subg2
error
4. is_solved error
si 8. subgoals
6. is_solved error
9. is_solved error
o ut
subgoals
l
l _a mp
.a 10
3 subgoals
5. auto
l al p_ m i .s
subgoals 11. is_solved error
Fig. 18. The implicit OR-tree exploration of try-to-prove for revs_eq.
try-to-prove implements a backtracking search over three sub-strategies: one based on a general-purpose tactic (auto), the second based on proof by induction, and the last one using sledgehammer [4]. Its search path of try-to-prove is shown in Fig. 18 schematically. In this figure, numbers in the edge labels represent the order of implicit tree traversal, and dashed edges represent the failures of tactic applications, which triggers backtracking. As the numbers on the edges and the single-lined node edges illustrate, the PSL’s interpreter executes the depth-first search based on try-to-prove but fails to find a proof for revs_eq. The Ors combinator implements deterministic choice, and as soon as the PSL interpreter finds an atomic proof using Algorithm 3, it stops the search, as a single atomic proof suffices to complete the OR-node. 4.3
Implicit Conjecturing using exp-tactic: Tactics to Expand OR-leaf nodes.
Contrary to try-to-prove in Algorithm 3, exp-tactic in Algorithm 4 attempts to expand the ORnode by taking all successful leaf nodes as shown in Fig. 19. This time, only one leaf is surrounded by dashed boundary and pointed to by a dashed edge. That is, only one leaf node represents the complete failure of tactic application, while other nodes contain viable subgoals that are at least aligned with MP-tac from Section 2.1. That is, even though these leaves do not represent the completion of proof search either; they can be used to expand the abduction graph. Note that both Algorithm 3 and Algorithm 4 are executed by PSL, which is based on the OR-tree model. As such, each node produced by Algorithm 4 may or may not contain multiple subgoals. For this reason, the OR-nodes generated by Algorithm 4 are first incorporated into the abduction graph as AND-nodes. Then, the Prover decomposes each AND-node from Algorithm 4 into separate OR-nodes within the abduction graph, after confirming that treating the remaining subgoals as independent conjectures allows us to complete the newly added AND-node. This transition from the local use of the OR-tree model to the global use of the AND-OR graph model is illustrated in Fig. 20. This figure integrates the OR-leaf node, highlighted with a yellow background in Fig. 19, as a yellow AND-node in Fig. 20. Note that the label from revs_eq to subgoals in Fig. 20 is the concatenation of the labels from revs_eq to subgoals in Fig. 19, followed by the tactic application (simp add: subgoal) required to complete subgoals , assuming subgoals .
16
Nagashima et al.
revs_eq. rev1 𝑥𝑠 [] = rev2 𝑥𝑠 a 1. cl
error
p
rsim
5. i nd uc t
t
2.
uc nd
i
subg1’∧subg2’
subg1∧subg2
4. auto
to au
3 subgoals
l al
7.
l
al
p_ im .s
𝑥𝑠
_ mp si
6. subgoals
subgoals
subgoals
Fig. 19. Expansion of revs_eq using Algorithm 4 (exp-tactic).
revs_eq. rev1 𝑥𝑠 [] = rev2 𝑥𝑠 ...
... induct 𝑥𝑠, simp_all, simp add: subgoal subgoals subgoals Fig. 20. Integration of OR-nodes into Abduction Graph.
Algorithm 5 jackhammer
Algorithm 6 refute
1: Thens [ 2: Repeat ( Hammer ), 3: IsSolved 4: ]
1: Thens [ 2: Quickcheck, 3: Nitpick 4: ]
Notice that it is not guaranteed that the simp tactic can always accomplish this task in the general setting. Therefore, the AbductionProver determines the necessary tactics and their arguments by running sledgehammer on the AND-node after temporarily assuming all its child OR-nodes in the background context using the PSL strategy called jackhammer described in Algorithm 5. This PSL strategy invokes sledgehammer as many times as possible until sledgehammer fails. For this specific subgoal, it calls sledgehammer once, obtains the tactic (simp add: subgoals), and stops because this tactic application discharges the only remaining subgoal. 5
System Description B: Explicit Conjecturing
Section 4 introduced how to gradually expand abduction graphs using PSL and tactics. As discussed in Section 2.4, we consider such tactic applications as a form of implicit conjecturing. The key distinction between implicit and explicit conjecturing lies in how the relevance of conjectures (denoted as C1 in Section 2.3) is verified. Implicit conjecturing relies on the underlying prover’s mechanism to ensure that the left-hand branch of the derivation tree (MP-tac) in Section 2.1 holds, thereby automatically granting the relevance of conjectures. In contrast, explicit conjecturing
Abduction Prover in Isabelle/HOL
17
requires us to explicitly filter conjectures based on their relevance by proving the left-hand branch of the derivation tree (MP-conj) in Section 2.3, as we will see in Section 6.2. Currently, the AbductionProver employs two approaches for explicit conjecturing: template-based conjecturing and mutation-based conjecturing. 5.1
exp-template: Template-Based Conjecturing.
In template-based conjecturing, embodied as exp-template, AbductionProver first collects relevant functions and generates conjectures based on 16 pre-defined templates. These templates parametrically describe common patterns such as associativity, commutativity, reflexivity, and distributivity, without being specific to any particular problem domain. While our template-based conjecturing approach in AbductionProver builds upon the earlier work of Nagashima et al., the direction of reasoning differs fundamentally. Nagashima et al. employed template-based conjecturing in a bottom-up manner, focusing on generating and proving conjectures from available functions and data types using the default, extensive PSL strategy, independently of the original goal. In contrast, AbductionProver adopts a top-down goal-oriented approach, assessing the relevance of conjectures via Modus Ponens, as discussed in Section 2.3. Even if the default, less extensive PSL strategy (Algorithm 3) fails to establish an atomic proof for a conjecture, AbductionProver retains it as an OR-leaf, enabling further proof efforts through recursive conjecturing. A known limitation of the template-based approach discussed in the literature is its lack of specificity to a given problem. For example, the helper lemma from Section 2.3 does not fit into any of the predefined templates, yet it closely resembles the original goal, revs_eq. 5.2
exp-mutation: Mutation-Based Conjecturing.
Mutation-based conjecturing addresses this limitation by generating conjectures through mutations of the current goals. Since all mutants originate from the goals (OR-leaves), this approach aims to maintain a degree of specificity to them. Currently, the AbductionProver employs the following six mutation algorithms: 1: Remove outermost assumption. Strips away the outermost implication (or assumption) to obtain a more direct statement. This may remove useful terms from the assumption that could help prove the conclusion, but it may also provide a clearer focus on the conclusion for the subsequent steps. Example: Input: rev1 𝑥𝑠 [] = rev2 𝑥𝑠 =⇒ rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠) Output: rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠) 2: Remove function. Strips away the outermost implication (or assumption) to obtain a more direct statement. This may remove useful terms from the assumption that could help prove the conclusion, but it may also provide a clearer focus on the conclusion for the subsequent steps. Example: Input: rev1 𝑥𝑠 𝑦𝑠 = rev2 𝑥𝑠 + 𝑦𝑠 Output: rev1 𝑥𝑠 𝑦𝑠 = 𝑥𝑠 + 𝑦𝑠 3: Abstract same term. Identifies identical or repeated sub-terms and replaces them with a fresh variable. This reduces redundancy and highlights the common sub-term, making the goal potentially simpler to manipulate. However, it may also eliminate information that is useful for completing the proof. Example: Input: rev1 𝑥𝑠 [] = rev2 𝑥𝑠 =⇒ rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠) Output: rev1 𝑥𝑠 [] = rev2 𝑥𝑠 =⇒ rev1 𝑦𝑠 [] = rev2 𝑦𝑠
18
Nagashima et al.
4: Replace implication with equation. Rewrites an implication as an equation. In general, this makes the goal harder to prove; however, the stronger goal based on an equation can occasionally open up alternative inference paths or simplifications. Example: Input: rev1 𝑥𝑠 [] = rev2 𝑥𝑠 =⇒ rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠) Output: (rev1 𝑥𝑠 [] = rev2 𝑥𝑠) = (rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠)) 5: Generalize by renaming variables. Renames some occurrences of variables to fresh variables when the goal contains multiple occurrences of the same variable. While this mutation makes the goal stronger, the resulting statement is sometimes better aligned with certain proof procedures, such as proof by induction. Input: rev1 𝑥𝑠 [] = rev2 𝑥𝑠 =⇒ rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑥𝑠) Output: rev1 𝑥𝑠 [] = rev2 𝑦𝑠 =⇒ rev1 (𝑥1:𝑥𝑠) [] = rev2 (𝑥1:𝑦𝑠) 6: Generalize, then extend. Generalizes the goal by replacing constants with variables, then extends it by replacing a subterm of the goal with a composite term that applies a function to the original subterm. This mutation algorithm selects such functions from the list of registered functions in the proof context based on their relevance to the functions appearing in the input goal. Currently, the algorithm considers functions that appear in the definitions of the used functions as relevant. For the following example, the algorithm selects the function (+) from the proof context because this function is used in the definition of rev2. Example: Input: rev1 𝑥𝑠 [] = rev2 𝑥𝑠 Generalized: rev1 𝑥𝑠 𝑦𝑠 = rev2 𝑥𝑠 Output: rev1 𝑥𝑠 𝑦𝑠 = rev2 𝑥𝑠 + 𝑦𝑠 This mutation was first proposed by Nagashima et al. [3] and sometimes produces broader statements that relate previously unconnected parts of the proof context. Note that although we have shown only one example output for each input, these algorithms generally produce numerous candidate conjectures from a single subgoal. 6
System Description C: Conjecture Filtering
The aforementioned conjecturing approaches, particularly the mutation-based algorithm, tend to generate a large number of candidates. While the graph structure presented in Section 2 helps mitigate the combinatorial explosion by enabling node-sharing, the sheer volume of candidates still necessitates additional filtering strategies. As such, the AbductionProver employs many filtering approaches step-by-step. 6.1
Abductive Reasoning: Filtering Based on Modus Ponens
The central filtering method of the AbductionProver is based on the Modus Ponens as discussed in Section 2.3: we want conjectures that are useful (C1) but not equivalent to False (C2). Filtering based on Counterexample Finders. Similarly to previous work in this field, we use available counterexample finders (Quickcheck and Nitpick) to filter out false conjectures using the PSL program, refute, shown in Algorithm 6. Algorithm 6 sequentially combines two substrategies: Quickcheck and Nitpick. This ordering ensures that the Prover invokes Nitpick only if Quickcheck finds no counterexamples, thereby improving overall performance, as Nitpick is often more computationally expensive than Quickcheck. The results are stored in a lookup table, separate from the main data structure—the abduction graph introduced in Section 3, to avoid repeatedly invoking the resource, intensive counterexample finders on identical conjectures generated from different branches of the abduction graph.
Abduction Prover in Isabelle/HOL
19
round 1
round 2
round 3
round 4
conjecture-1 conjecture-2 conjecture-3 conjecture-4
conjecture-1 conjecture-2 conjecture-4
conjecture-1 conjecture-3
conjecture-1
conjecture-1 conjecture-3 conjecture-4
conjecture-1 conjecture-4
Fig. 21. Successive Proof-Guided Conjecture Set Identification. In these four rounds, the AbductionProver identifies 4 sets of provably useful conjectures: {conjecture-2}, {conjecture-2, conjecture-3}, {conjecture-3}, {conjecture-3, conjecture-4}.
This use of counterexample finders addresses the right branch of the derivation tree (MP-conj) in Section 2.3, which corresponds to the C2 requirement presented in the same section. One-Step Abduction. On the other hand, one-step abduction addresses the left branch of the derivation tree (MP-conj) in Section 2.3, which corresponds to the C1 requirement presented in the same section. The AbductionProver achieves this by temporarily assuming the conjectures under consideration and attempting to prove the goal using these assumptions. Contrary to previous work on abductive reasoning in Isabelle [3], which inserts conjectures as assumptions within the corresponding goals and attempts to prove the resulting goals using the fastforce tactic, the AbductionProver instead registers conjectures axiomatically in the underlying proof context and attempts to prove the respective goal within this context using sledgehammer. This shift enables the AbductionProver not only to leverage the strong proof automation of sledgehammer but also to efficiently exploit multiple conjectures simultaneously, identifying useful conjecture combinations rather than a single useful conjecture, using successive proof-guided conjecture set refinement explained below. 6.2
Successive Proof-Guided Conjecture Set Identification using sledgehammer
When we introduced one-step conjecturing in Section 2.3, it was presented as if the AbductionProver would check the relevance (C1) of each single candidate conjecture separately. Indeed, that was the approach taken by the previous work on abductive reasoning in Isabelle [3]; however, checking individual conjectures in isolation suffers from two key issues: • Scalability concerns: When numerous conjectures are present, evaluating the left branch of MP-conj (conj =⇒ goal) separately for each conjecture leads to significant performance degradation. • Dependency among conjectures: While some goals require a set of conjectures simultaneously to be completed, a naive application of explicit single conjecturing does not inherently provide these sets. The second limitation stands in stark contrast to tactic applications, which act as implicit conjecturing: a single tactic application may generate multiple subgoals (conjectures), all of which must be proven. In contrast, when generating multiple conjectures explicitly, it is not immediately clear which subsets must be proven. The number of potential subsets grows combinatorially, making brute-force evaluation impractical for large conjecture spaces.
20
Nagashima et al.
To address these issues, we developed a method called successive proof-guided conjecture set identification. In this approach, we temporarily assume all conjectures that pass the initial screening and register them in the underlying proof context. We then run sledgehammer to determine whether it can prove the current goal using any of these assumed conjectures. If sledgehammer finds a proof script, AbductionProver extracts the conjectures used in the proof and generates alternative conjecture sets by removing one used conjecture from the previous set for each alternative set. This process repeats iteratively until either sledgehammer fails to find a proof for all candidate subsets or the iteration reaches a predefined limit, currently set to 15 for the root node and 5 for other OR-nodes This iterative process is illustrated in Fig. 21 schematically using an abstract scenario. This figure shows that the process starts with the four conjectures each named conjecture-𝑛. In the first round, sledgehammer finds a proof script involving two of them (conjecture-2 and conjecture-3) and registers this subset as a candidate AND-node. Then, it produces two subsets by removing one of these conjectures for each subset. In the second round, the process runs sledgehammer with these subsets of cardinality 3 against the same goal. For the first subset, sledgehammer found a script involving conjecture-2, while it found a script involving conjecture-3 and conjecture-4. Therefore, the process registers the two subsets (conjecture-2 and conjecture-3, conjecture-4) as candidate for AND-nodes. The third round and fourth round proceed similarly, while each round involves subsets using which sledgehammer fails to prove the current goal, leading to the end of the iterative process. Note that despite its iterative nature, successive proof-guided conjecture set identification constitutes a single one-step conjecturing process. For example, the four sets of conjectures identified in Fig. 21 serve as candidate child AND-nodes for a single parent OR-node. Within each iteration of the main loop, presented in Section 4.1 as Algorithm 1, AbductionProver applies successive proof-guided conjecture set identification to each OR-node selected by get-contributive-leaves. 6.3
Filtering Beyond Abductive Reasoning
Successive proof-guided conjecture set identification generates many conjectures that are either false or redundant. To mitigate combinatorial explosion, the AbductionProver incorporates several additional filtering mechanisms beyond abductive reasoning, including: type-guided conjecturing, 𝛼-normalization, simplifier-normalization, and history-sensitive pruning. Due to space limitations, we refrain from describing these mechanisms in detail in this paper. 7
Conclusion
This paper presented the AbductionProver for Isabelle/HOL, a proof-search framework based on recursive abductive reasoning over AND-OR graphs. The framework uniformly treats tactic applications and explicit conjecturing as instances of Modus Ponens, enabling proof search through the expansion of abduction graphs while tracking completion and contributivity statuses of nodes. We extended the standard OR-tree interpretation of tactical theorem proving to AND-OR graphs to support recursive conjecturing and the sharing of intermediate lemmas across proof branches. The AbductionProver combines local OR-tree exploration using PSL with global graph-based reasoning, supports cyclic abduction graphs together with acyclic solution extraction, and integrates multiple techniques for conjecture generation, normalization, and pruning. This paper focused on clarifying the computational model and architectural design of the AbductionProver through a running example and algorithmic descriptions. A working implementation for Isabelle/HOL is publicly available. Overall, the current implementation suggests that graph-based abductive reasoning is a promising direction for proof automation in tactical theorem provers.
Abduction Prover in Isabelle/HOL
21
References [1] Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. 378–388. doi:10.1007/978-3-319-21401-6_26 [2] Yutaka Nagashima and Ramana Kumar. 2017. A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings (Lecture Notes in Computer Science, Vol. 10395), Leonardo de Moura (Ed.). Springer, 528–545. doi:10.1007/978-3-319-63046-5_32 [3] Yutaka Nagashima and Julian Parsert. 2018. Goal-Oriented Conjecturing for Isabelle/HOL. In Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11006), Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (Eds.). Springer, 225–231. doi:10.1007/978-3-319-96812-4_19 [4] Lawrence C. Paulson and Jasmin Christian Blanchette. 2010. Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011 (EPiC Series in Computing, Vol. 2), Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska (Eds.). EasyChair, 1–11. doi:10.29007/36dt [5] Konrad Slind and Michael Norrish. 2008. A Brief Overview of HOL4. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings. 28–32. doi:10.1007/978-3-54071067-7_6 [6] The Coq development team. 1984. The Coq Proof Assistant. https://coq.inria.fr