This paper introduces a framework for integrating Reinforcement Learning (RL) with proof search in connection calculi for classical, intuitionistic, and modal logic. We specify a mapping from the relevant connection calculi to Markov Decision Processes (MDPs), and provide a Python library implementing http://www.cl.cam.ac.uk/~fr409 (F. Rømming); http://jens-otten.de/ (J. Otten); http://www.cl.cam.ac.uk/~sbh11 0000-0001-7545-4662 (F. Rømming); 0000-0002-4331-8698 (J. Otten); 0000-0001-7979-1148 (S. B. Holden) Workshop Proceedings htp:/ceur-ws.org CEUR Workshop Proceedings (CEUR-WS.org) ISN1613-073
CEUR ceur-ws.org
Automated Theorem Proving (ATP) is concerned with determining whether a given formula is
valid in a specific logic. Complementary to classical logic, intuitionistic logic is used within
interactive proof assistants such as NuPRL [
non-classical logics exist, even though applications would benefit from more
eficient ATP systems. One approach to dealing with these non-classical logics is to encode
their Kripke semantics with prefixes [
Combining ATP and Machine Learning (ML) can enhance existing ATP systems (or theorem
provers) [
This paper introduces a framework for integrating Reinforcement Learning (RL) with proof search in connection calculi for classical, intuitionistic, and modal first-order logic. There are two main contributions: 1. The discussion and definition of a mapping from classical and non-classical connection calculi to Markov Decision Processes (MDPs). 2. A Python library implementing such MDPs providing seamless integration with the ML ecosystem facilitating RL experiments for in-prover guidance.
We introduce the connection calculi and ML techniques in Section 2. Section 3 specifies a mapping from proof search to the RL setting. Section 4 describes the implementation of the library. The paper concludes with a summary and a plan for future work in Section 5.
The following methods are based on uniform clausal connection calculi for classical, intuitionistic
and modal logic. We provide a short overview of these calculi; more details can be found
in [
An atomic formula (denoted by ) is built up from predicate symbols (denoted by , , ),
function symbols and term variables (, ). A (first-order) formula (denoted by ) is built up from
atomic formulae, the connectives ¬, ∧, ∨, ⇒, and the first-order quantifiers ∀ and ∃. A modal
formula might also include the modal operators □ and ◇. A literal has the form or ¬ . In
the (clausal) connection calculus a formula is represented as a matrix, which is a representation
of the formula in a (prefixed) clausal form.
2.1.1. Classical Logic
The classical matrix ( ) of a formula is its representation as a set of clauses, where each clause
is a set of literals. It is the representation of in disjunctive normal form, where Skolemization
of the eigenvariables [
The axiom and the three rules of the (clausal) connection calculus are given in Figure 1 (the
prefixes ∶ 1 and ∶ 2 are to be ignored for classical logic) [
Start (S) 2, , {} , , and 2 is copy of 1∈ Reduction (R) , , ℎ∪{
2∶ 2} ∪{ 1∶ 1}, , ℎ∪{ 2∶ 2}
and { 1∶ 1, 2∶ 2} is -complementary Extension (E) 2⧵{ 2∶ 2}, , ℎ∪{
1∶ 1} , , ℎ
∪{ 1∶ 1}, , ℎ
and 2 is a copy of 1∈ , 2∶ 2∈ 2,
{ 1∶ 1, 2∶ 2} is -complementary
2.1.2. Non-Classical Logics
For intuitionistic and modal logic, the matrix and the calculus are extended by prefixes,
representing world paths in the Kripke semantics; see [
) and constants (denoted by , ) and assigned to each literal.
Skolemization is not only used for the (first-order) eigenvariables, but extended to prefix
constants [
A prefix substitution assigns strings to prefix variables and is calculated by a prefix
unification that depends on the specific non-classical logic [
, 2∗ ∶= 2( ) , 2∗ ∶= 2( ) .1 graphical representation and graphical connection proof with the term substitution () = and the prefix substitution ( 1) = 2 , ( 2) = 2∗, ( 3) = 1∗, ( 4) = 2∗ (literals of each ∗ connection are connected with a line).
. It has the ∗ 1 3}, { 1∶ 4} } has the following 0 ∶ 2∗ [ [ 0 ∶ 2∗] [ 0∶ 1 ∶ 1 1∗ 1∗] [ 1∶ 1 ∶ 2
1 1∗ 3] [ ∶ 4] ] The formal connection proof of (where prefixes have been omitted for better readability) is shown in Figure 2.
1The polarities 0 and 1 are used to mark non-negated and negated literals, respectively (see [
1 { }, , { 0 0, 0 ′} A , 0 ′} R {
We now provide an introduction to MDPs and RL—details can be found in [
Most proof procedures are search algorithms: there is an initial state, states can be modified by actions, and the goal is to find a proof state. The use of heuristics is crucial for performance. For example, in the case of saturation provers, for choosing a pair of clauses to resolve. One might imagine an agent, armed with a heuristic, acting to change the initial state of its environment into a state representing a proof.
An MDP represents a more general formulation of this kind of problem. Let denote the set the environment moves to a new state ′ ∈ with probability ( ′ |, ) ; that is, ′ ∼ ( of states, and let denote the set of actions. When an agent performs action ∈ in state ∈ , At the same time, the agent receives a reward ℛ( ; , ) ∈ ℝ . The tuple (, , , ℛ) ′ |, ) .
defines ′ the MDP. Let subscripts denote the sequence of states, actions and rewards through time, and imagine the agent has a policy ∶ →
telling it which action to employ in any given state; that is, at time the agent always applies = ( ).2 Then, starting from a state 0, the agent will move through states
0 → 1 ∼ ( 1| 0, ( 0)) → 2 ∼ ( 2| 1, ( 1)) → ⋯ and receive a sequence of rewards
0 = ℛ( 1; 0, ( 0)) → 1 ∼ ℛ( 2; 1, ( 1)) → ⋯ .
A utility function
() computes the overall accumulated reward associated with the use of ,
starting from state . As future rewards are often perceived as less valuable than short-term
rewards, a common function is
() = [ 0 + 1 + 2 2 + ⋯] = [∑ ]
∞
=0
where the expected value is with respect to the randomness governing the state transitions,
⋆ is one satisfying ⋆() = argmax
() , and which leads to utility
() .
and ∈ [
Both the optimal policy and its corresponding utility can be expressed by considering what happens if we take particular actions from the current state and follow the optimal policy thereafter ′ ′ ⋆
() = max ∑ ( ′|, ) (ℛ( ′; , ) + ⋆() = argmax ∑ ( ′|, ) (ℛ( ′; , ) +
⋆ ( ′))
⋆ ( ′)) .
Numerous algorithms exist for inferring an optimal policy for an MDP, depending on what is known about the MDP. If little is known, we must learn about the environment by exploring actions and their efects, and this is what RL achieves.
As described in the previous section, RL concerns agents interacting with environments. In the case of proof procedures, one can consider an agent deciding which choice to make at each point in the proof search. Hence, to apply RL we need to define the proof search environment and its choice points. We now address the description of proof search procedures in connection calculi using MDPs.
While the reader familiar with the connection calculus might be tempted to see the relationship between proof and MDP as straightforward, it is in fact more subtle than is apparent at first glance, and requires some care to define correctly. While the connection calculi define procedures whereby sequential decisions are made to find proofs, they do not directly define MDPs. For confluent proof calculi such as resolution, one can treat the words of the calculus as observations and inference rules as actions, since all information about the state of the proof is carried in the most recently generated word. However, this cannot be done with connection calculi, because it is unclear how to handle branching and backtracking. The words of the connection calculi do not carry enough information to know whether the current state is a goal state (a proof), or to know what inferences have or have not been attempted. Allowing dead-end states that are not proofs would be unfaithful to the underlying dynamics (provers run until they have found a proof), so backtracking should be incorporated as part of the MDP.
We now specify the state space, action space, transition space, and reward function tuple (, , , ℛ)
for CC-MDP, one possible MDP representation of proof search in connection calculi. Definition 1 (CC-MDP State Space). The state space is defined as the set of all possible derivations (a derivation is an incomplete proof in which some leaves are not closed by axioms) in the connection calculus together with the substitution = . Further, to keep track of the open backtracking choices, each node in the connection derivation is marked with the possible inference steps that have not been attempted so far.
In general, there might be exponentially many unifiers for one prefix equation (of one
connection) [
Definition 2 (CC-MDP Action Space). The action space consists of rule application actions inferences and a backtracking action . There is a rule application action for each rule in the connection calculus. Hence, a rule application action , ∈ inferences is specified by the rule name ∈ {, , } (for Start, Reduction or Extension) and the associated clause and/or literal . Specifically, an action , can have one of the following forms: , 2 for the Start rule, , 2 for the Reduction rule and , 2/ 2 for the Extension rule.
Example 3. To get from the initial state , , to the state in Figure 3 one can take the actions: ,{,} , ,{¬, ′}/¬ , ,{¬,¬}/¬ . These actions are a start step with the clause { , } , followed by two extension steps connecting the leftmost literal 3 in the leftmost open subgoals of the proof tree to the literal in the clause {¬ , ′} and the literal ¬ in the clause {¬, ¬ } .
We say that action is valid in state if action = backtrack or is a rule application
action , ∈ inferences denoting a valid rule application to the leftmost literal in the leftmost
open subgoal in the proof tree of . A valid rule application takes the rigid term substitution
into account, so ( 1) = ( 2). As for the states in the state space , the rigid prefix
substitution is not taken into account (and updated) for the non-classical logics. To handle
proper backtracking, when a rule application action is taken from state to ′, is no longer
counted as a non-attempted inference for the node in the tableau of ′ corresponding to the
principal node [
In general an MDP models state transitions stochastically—performing action in state leads to a new state ′ ∼ ( ′|, ) . In a connection prover the transition is deterministic, in the sense that performing action in state leads reliably to a single outcome state ′. This gives rise to the following deterministic state transition function.
3All clauses (including subgoal clauses) are treated as ordered sets of literals. Definition 3 (CC-MDP Transition Function). The transition distribution is defined as ( ′ = ′|, ) = ⎧1 ⎨ ⎩0 if is valid in and ′ is the (deterministic) result of applying to otherwise.
Notice that the transition function is necessarily deterministic, as any probabilistic transition function would not accurately describe the dynamics of the underlying system.
We only consider the first literal of the leftmost open subgoal for rule application. This is because all subgoals need to be closed, so we do not consider alternative subgoals and literals within subgoals as choice points for the MDP. Including these as choice points could be interesting, but it would also increase the size of the action space and general complexity introducing a trade-of.
Definition 4 (CC-MDP Reward Function). To remain faithful to the underlying problem, we consider the following relatively sparse reward function ℛ( ′; , ) = where ′ is a proof if the derivation of ′ is a proof under the unique (combined) substitution = (for classical logic) or = ( , ) of ′.
This reward function is the simplest function accurately describing the goal while preserving optimality of solutions.
Example 4. Figure 4 shows the graph representation of a part of CC-MDP.
ε, {{P, R}, {¬P, Qx}, {¬P, ¬Qc}, {¬R}}, ε
aS,{P,R} {P, R}, M, {} ε, {{P, R}, {¬P, Qx}, {¬P, ¬Qc}, {¬R}}, ε
S aE,{¬P,¬Qc}/¬Qc {¬Qc} , M, {P } {R}, M, {} E
{P, R}, M, {} ε, {{P, R}, {¬P, Qx}, {¬P, ¬Qc}, {¬R}}, ε
S {Qx′} , M, {P } {R}, M, {} E
{P, R}, M, {} ε, {{P, R}, {¬P, Qx}, {¬P, ¬Qc}, {¬R}}, ε
S aE,{¬P,Qx}/¬P aE,{¬P,¬Qc}/¬Qc {¬P }, M, {P, Qx′} {}, M, {P } E {Qx′} , M, {P }
{P, R}, M, {} ε, {{P, R}, {¬P, Qx}, {¬P, ¬Qc}, {¬R}}, ε
S {R}, M, {} E
Proof search in the classical and non-classical connection calculi can be framed as an agent interacting with the CC-MDP environment, giving the necessary theoretical framework for applying RL to the proof search in these connection calculi. Furthermore, techniques such as positive start clauses and iterative deepening can be accounted for with minor tweaks to the components of CC-MDP.
Connections [
Connections implements the basic calculi for classical, intuitionistic, and modal logic as
described above, enhanced by regularity [
ConnectionEnv
Prover agent action state reward Connections
Connection Environments Unification Logical primitives
Matrix ConnectionAction
ConnectionState Term unification
Prefix unification (D, T, S4, S5, Intuitionistic)
Literal
Term
Compared to conducting learning experiments with external calls to Prolog and OCaml
implementations of leanCoP, using the Connections environments drastically reduces the complexity
needed to control the prover. This is due to eliminating the need for remote procedure calls, and
to the imperative basis of the environments, which allow fine-grained control while respecting
abstraction levels. Furthmore, using an imperative language to implement Connections allows
a more direct control of the proof search, e.g. of backtracking, than is possible in the declarative
Prolog programming language (see also [
The non-classical Connections environments inherit from the classical environment, adding logic-specific prefixes and prefix unification algorithms. The non-classical provers based on Connections perform a classical proof search, in which the prefixes of the literals in each connection are collected. After a classical proof is found, these prefixes are unified by a prefix unification algorithm to ensure that the classical proof is also a valid non-classical proof.
Besides the basic calculi, the Connections environments implement two additional
wellknown optimizations, significantly reducing the underlying search space while preserving
completeness. The start clause 1/ 2 of the start rule is restricted to positive start clauses (those
without negated literals, which likely represent conjecture clauses in the disjunctive normal
form) and the regularity condition [
The Connections environments are not provers by themselves; they expose an interface that agents can use to train and make inferences, completing the RL agent-environment interaction loop, as shown in Figure 5. A prover in this context is an agent making consecutive steps in a Connections environment until it has found proof or timed out.
The Connections environments can be used to build both learning and non-learning connection provers, depending on the agent used. For example, by using non-learning agents that always choose the first available action, we obtain standard Python connection provers in an elegant and straightforward way—the provers emerge from the interaction between the “always-first” agent and a Connections environment. The complete Python code implementing such a prover is shown in Figure 6. env = ConnectionEnv("problem_path") observation, info = env.reset() while True: action = env.action_space[0] # Always choose first available action observation, reward, terminated, truncated, info = env.step(action) if terminated or truncated:
break
Depending on the environment used (ConnectionEnv, IConnectionEnv or MConnectionEnv)
this results in three (stand-alone) Python provers [
While the main purpose of the Connections environments is to facilitate easy implementation of learned provers for classical, intuitionistic, and modal logic using the MDP + agent view of connection proof search, the pyCoP provers highlight the general (learning and non-learning) capabilities of the Connections environments and give confidence in the correctness of their implementation by showing that they can be used to emulate leanCoP, ileanCoP, and MleanCoP.
We present a Python library providing a framework for ML in connection calculi for classical and non-classical logics, and with specific emphasis on facilitating experiments using RL to guide proof search. Aside from its ML-centric component, this also represents the first non-Prolog implementation of provers based on the clausal non-classical connection calculi, and using prefix unification to capture the Kripke semantics of intuitionistic and modal first-order logics.
We are at present using this library to experiment with RL methods in an attempt to improve the performance of the unmodified provers, and we hope that the library inspires and facilitates others to explore their own ideas within this space.
In future work, we intend to extend the library to allow us more fully to address restricted
backtracking, refutation techniques, and to include both further modal logics, and non-clausal
methods such as those of nanoCoP [