Embedded Files
Summary of our research
Summary of our research
We present a reinforcement learning based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP focuses on generalizing from short proofs to longer ones of similar structure. To achieve that, FLoP uses state-of-the-art RL approaches that were previously not applied in theorem proving. In particular, we show that curriculum learning significantly outperforms previous learning-based proof guidance on a synthetic dataset of increasingly difficult arithmetic problems.
The proof engine used by FLoP is based on a connection calculus and specifically on leanCoP and its OCaml implementation introduced in FEMaleCoP. Using two simple examples we illustrate below how a proof looks like in our system and at the same time the examples illustrate what kind of problems appear in the dataset on which FLoP is trained. The dataset and the training algorithm are described in details in the paper. Here let us mention, that the algorithm is based on Backplay and "Learning Montezuma’s Revenge from a Single Demonstration". The dataset is based on Robinson Arithmetic and consists of 3 stages described below.
In the paper we also describe five experiments. In Experiment 1 we show that FLoP can learn from a single training proof. In Experiment 2 we show that FLoP is more robust than supervised learning on training proofs. In Experiment 3 we demonstrate that FLoP can learn when no proof is provided, only the training problems. In Experiment 4 we compare FLoP with other provers (E, Vampire, leanCoP, rlCoP) and show that it performs very well on the arithmetic datasets. In Experiment 5 we show that FLoP tends to solve problems in fewer steps than rlCoP and also solves problems that require significantly longer proofs. We also discuss some failure modes.
Code is accessible via github: https://github.com/atpcurr/atpcurr - the repository contains almost all pieces of relevant software with two notable exceptions: 1) the binary with the OCaml engine 2) the experiment runner. The binary cannot be publicly released at this time and is distributed on request. The runner is directly linked to our hardware infrastructure and would be useless elsewhere.
The dataset
The dataset
We introduce a suite of problems in the theory of Robinson Arithmetic. This theory is rather limited, however, it seems to be particularly suited for machine learning methods: solutions are long, repetitive and rather predictable for humans. Still, as our paper shows in the Experiments section, state-of-the-art systems struggle to solve some of these problems.
The dataset can be downloaded from our repository: https://github.com/atpcurr/atpcurr. We are using simple, synthetic datasets, which makes it very easy to generate different variants. The codebase also includes a problem generator which can be used easily to generate problems in Robinson Arithmetic with different difficulties. (See the codebase readme for usage details.)
Each problem can be viewed as a separate environment and a guidance system is expected to learn on some of them and then perform well in unseen environments, which is a meta-learning task. The problem sets are intended to be a general purpose testing ground for theorem proving and RL methods, in particular for meta-learning and hierarchical learning algorithms.
Curriculum learning on proof length
Curriculum learning on proof length
In theorem proving we are dealing with sparse rewards and we tackle this with the help of curriculum learning. We aim to build a learning algorithm that strikes a good balance between exploiting prior knowledge and exploration. Prior knowledge comes from proofs that are either provided or previously found by the system. We argue that making good use of this knowledge is crucial in order to solve harder problems.
Fully formalized mathematical proofs can easily get thousands of steps long, and any guidance based on superficial statistics extracted from the training data will have an exponentially diminishing chance of succeeding as the length increases. The guidance has to be ''fully confident'' on large parts of the proof, which essentially requires learning of rule like associations. Other parts of the proof, however, may require more flexibility, where it is meaningful to create choice points and explore different alternatives.
Given a training proof, we start exploration from the end of the proof, making it easy to succeed and obtain positive reward. As the system gets more confident, we gradually move the starting state backwards along the given proof.
Comparison with other theorem provers
Comparison with other theorem provers
We compare FLoP with two state-of-the-art saturation-style theorem provers (E, Vampire), a strong connection tableau prover (leanCoP) and one connection tableau prover using learning-based guidance (rlCoP).
Vampire, E and leanCoP use human-designed strategies instead of learning. In our tests we use the casc mode for Vampire, the auto and auto-schedule modes for E and the default collection of 40 strategies for leanCoP, each with a timeout of 60 sec. per problem. For rlCoP we used the same hyperparameters as those described in their paper, only modifying the policy temperature from 2.5 to 1.5. The number of inferences in the Monte Carlo Tree search was limited to 200000. For Stage 1 and$2 rlCoP was run directly on the evaluation set. For Stage 3 all problems were too hard to solve without guidance within the inference limit, so we started with the version trained on the solutions of Stage $2$. For FLoP we report the best models trained without proofs. Success ratios are given in the table below.
E's auto-schedule tries multiple strategies and finds one with the left-to-right ordering of all the addition and multiplication axioms. This solves all of our problems immediately without any proof search by only using rewriting to a normal form. This demonstrates the power of equational theorem proving when a suitable term ordering exists and can be found by human-designed heuristics. This is however far from guaranteed in general and nontrivial even in such simple domains, as witnessed by Vampire's failure to find this ordering. To evaluate E without access to its built-in rewriting capability, we have renamed the equality to a new predicate `eq' axiomatized exactly in the same way as in FLoP and rlCoP. The auto-schedule mode then solves 54% problems in Stage 1, comparable to the auto mode.
Comparison of lengths of proofs
Comparison of lengths of proofs
We compare lengths of proofs found by FLoP and by rlCoP on problems in Stage 3. Comparisons with other provers are in principle possible, but rlCoP is the only prover which can be compared directly, because it uses the same proof system. Despite that our system is geared towards finding longer proofs, in fact it finds shorter proofs than rlCoP. rlCoP is based on Monte Carlo Tree Search with learned value and policy functions. The training procedure in rlCoP consist of iterative supervised training of these two functions. In the current training procedure of rlCoP there is no direct incentive to find shorter proofs and as a result FLoP finds not only more proofs, but overall these proofs are shorter. It is also interesting to notice that despite simplicity of our problems and proofs, apparently the systems never found exactly the same proof.
Screencast and logs showing a proof of the equality 1 x 1 = 1 along with comments and a figure
Screencast and logs showing a proof of the equality 1 x 1 = 1 along with comments and a figure
Below we show logs of an interactive session where a user types a proof of the equality 1 x 1 = 1.
At each step the proof state is shown:
'Cla' (list of literals): The goal that we are currently trying to prove. This corresponds to one unclosed tip of the tableau.
'Path' (list of literals): The branch of the tableau that leads to the current goal.
'Lem' (list of literals): Lemmas, i.e., previously proven literals that can be used to prove the current goal.
'Stk' (list of literals): Other unclosed tips of the tableau that will have to be visited after proving the current goal.
'Act i' (list of clauses): All the contrapositives that can be used in the next extension step. This constitutes the valid actons of the environment.
'Hashes': (list of integers): For portability, each contrapositive is associated with a unique hash value, which can be used to identify it, even if axioms are reordered. Hence, a list of action hash indices is a convenient representation of a proof.
The user has two kinds of actions:
'start()': restart the proof attempt
'step(i)': select the i-th contrapositive and make an extension step
(theorem) atpcurr@nvidia-server:~/theorem/curriculum_learning_theorems (master) $ python -i show_proof_states.py theorems/robinson/robinson_1m1__1/robinson_1m1__1.p Cla: ('#')Path: ()Lem: ()Stk: ()Act0: ((mul(s(o),s(o))=s(o)=>~'#'))======================================Index sequence: []>>> step(0)action 0Cla: (mul(s(o),s(o))!=s(o))Path: ('#')Lem: ()Stk: ()Act0: ((s(A)=s(B)=>A=B))Act1: ((A=B=>B=A))Act2: ((A=B=>(C=A=>C=B)))======================================(3, 0)>>> step(2)action 2Cla: (mul(s(o),s(o))!=A,A!=s(o))Path: (mul(s(o),s(o))!=s(o),'#')Lem: ()Stk: ()Act0: (mul(A,s(B))=plus(mul(A,B),A))Act1: ((A=B=>(C=D=>mul(A,C)=mul(B,D))))Act2: ((s(A)=s(B)=>A=B))Act3: (A=A)Act4: ((A=B=>B=A))Act5: ((A=B=>(C=A=>C=B)))======================================(6, 0)>>> step(0)action 0Cla: (plus(mul(s(o),o),s(o))!=s(o))Path: (mul(s(o),s(o))!=s(o),'#')Lem: (mul(s(o),s(o))!=plus(mul(s(o),o),s(o)))Stk: ()Act0: ((s(A)=s(B)=>A=B))Act1: ((A=B=>B=A))Act2: ((A=B=>(C=A=>C=B)))======================================(3, 0)>>> step(2)action 2Cla: (plus(mul(s(o),o),s(o))!=F,F!=s(o))Path: (plus(mul(s(o),o),s(o))!=s(o),mul(s(o),s(o))!=s(o),'#')Lem: (mul(s(o),s(o))!=plus(mul(s(o),o),s(o)))Stk: ()Act0: (plus(A,s(B))=s(plus(A,B)))Act1: ((A=B=>(C=D=>plus(A,C)=plus(B,D))))Act2: ((s(A)=s(B)=>A=B))Act3: (A=A)Act4: ((A=B=>B=A))Act5: ((A=B=>(C=A=>C=B)))======================================(6, 0)>>> step(0)action 0Cla: (s(plus(mul(s(o),o),o))!=s(o))Path: (plus(mul(s(o),o),s(o))!=s(o),mul(s(o),s(o))!=s(o),'#')Lem: (plus(mul(s(o),o),s(o))!=s(plus(mul(s(o),o),o)),mul(s(o),s(o))!=plus(mul(s(o),o),s(o)))Stk: ()Act0: ((A=B=>s(A)=s(B)))Act1: ((s(A)=s(B)=>A=B))Act2: ((A=B=>B=A))Act3: ((A=B=>(C=A=>C=B)))======================================(4, 0)>>> step(0)action 0Cla: (plus(mul(s(o),o),o)!=o)Path: (s(plus(mul(s(o),o),o))!=s(o),plus(mul(s(o),o),s(o))!=s(o),mul(s(o),s(o))!=s(o),'#')Lem: (plus(mul(s(o),o),s(o))!=s(plus(mul(s(o),o),o)),mul(s(o),s(o))!=plus(mul(s(o),o),s(o)))Stk: ()Act0: ((s(A)=s(B)=>A=B))Act1: ((A=B=>B=A))Act2: ((A=B=>(C=A=>C=B)))======================================(3, 0)>>> step(2)action 2Cla: (plus(mul(s(o),o),o)!=M,M!=o)Path: (plus(mul(s(o),o),o)!=o,s(plus(mul(s(o),o),o))!=s(o),plus(mul(s(o),o),s(o))!=s(o),mul(s(o),s(o))!=s(o),'#')Lem: (plus(mul(s(o),o),s(o))!=s(plus(mul(s(o),o),o)),mul(s(o),s(o))!=plus(mul(s(o),o),s(o)))Stk: ()Act0: (plus(A,o)=A)Act1: ((A=B=>(C=D=>plus(A,C)=plus(B,D))))Act2: ((s(A)=s(B)=>A=B))Act3: (A=A)Act4: ((A=B=>B=A))Act5: ((A=B=>(C=A=>C=B)))======================================(6, 0)>>> step(0)action 0Cla: (mul(s(o),o)!=o)Path: (plus(mul(s(o),o),o)!=o,s(plus(mul(s(o),o),o))!=s(o),plus(mul(s(o),o),s(o))!=s(o),mul(s(o),s(o))!=s(o),'#')Lem: (plus(mul(s(o),o),o)!=mul(s(o),o),plus(mul(s(o),o),s(o))!=s(plus(mul(s(o),o),o)),mul(s(o),s(o))!=plus(mul(s(o),o),s(o)))Stk: ()Act0: (mul(A,o)=o)Act1: ((s(A)=s(B)=>A=B))Act2: ((A=B=>B=A))Act3: ((A=B=>(C=A=>C=B)))======================================(4, 0)>>> step(0)action 0Cla: ()Path: ()Lem: ('#')Stk: ()======================================(0, 1)
Another useful take on formal proofs consists in drawing a graph of the proof. The above interactive proof suggests that we reason in a linear way, but in fact the system is performing splits into so-called subgoals and for a while forces the user to focus on a proof of a subgoal.
Screencast and log showing a proof of the equality 0 + 0 + 1 = 1
Screencast and log showing a proof of the equality 0 + 0 + 1 = 1
In our dataset we use the same set of axioms (see lines 1-6 in the formulation of the problem 0 + 0 + 1 = 1). The difference between problem files for 1 x 1 = 1 and 0 + 0 + 1 = 1 is only in the line with the conjecture, that is line 7 in the listing below.
(theorem) atpcurr@nvidia-server:~/theorem/curriculum_learning_theorems (master) $ python -i show_proof_states.py theorems/robinson/robinson_0p0p1__1/robinson_0p0p1__1.p Cla: ('#')Path: ()Lem: ()Stk: ()Act0: ((plus(o,plus(o,s(o)))=s(o)=>~'#'))======================================Index sequence: []>>> step(0)action 0Cla: (plus(o,plus(o,s(o)))!=s(o))Path: ('#')Lem: ()Stk: ()Act0: ((s(A)=s(B)=>A=B))Act1: ((A=B=>B=A))Act2: ((A=B=>(C=A=>C=B)))======================================(3, 0)>>> step(2)action 2Cla: (plus(o,plus(o,s(o)))!=A,A!=s(o))Path: (plus(o,plus(o,s(o)))!=s(o),'#')Lem: ()Stk: ()Act0: ((A=B=>(C=D=>plus(A,C)=plus(B,D))))Act1: ((s(A)=s(B)=>A=B))Act2: (A=A)Act3: ((A=B=>B=A))Act4: ((A=B=>(C=A=>C=B)))======================================(5, 0)>>> step(0)action 0Cla: (plus(o,s(o))!=G,o!=E)Path: (plus(o,plus(o,s(o)))!=plus(E,G),plus(o,plus(o,s(o)))!=s(o),'#')Lem: ()Stk: (plus(E,G)!=s(o))Act0: (plus(A,s(B))=s(plus(A,B)))Act1: ((A=B=>(C=D=>plus(A,C)=plus(B,D))))Act2: ((s(A)=s(B)=>A=B))Act3: (A=A)Act4: ((A=B=>B=A))Act5: ((A=B=>(C=A=>C=B)))======================================(6, 0)>>> step(0)action 0Cla: (o!=E)Path: (plus(o,plus(o,s(o)))!=plus(E,s(plus(o,o))),plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,s(o))!=s(plus(o,o)))Stk: (plus(E,s(plus(o,o)))!=s(o))Act0: ((s(A)=s(B)=>A=B))Act1: (A=A)Act2: ((A=B=>B=A))Act3: ((A=B=>(C=A=>C=B)))======================================(4, 0)>>> step(1)action 1Cla: (plus(o,s(plus(o,o)))!=s(o))Path: (plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,plus(o,s(o)))!=plus(o,s(plus(o,o))))Stk: ()Act0: ((s(A)=s(B)=>A=B))Act1: ((A=B=>B=A))Act2: ((A=B=>(C=A=>C=B)))======================================(3, 0)>>> step(2)action 2Cla: (plus(o,s(plus(o,o)))!=K,K!=s(o))Path: (plus(o,s(plus(o,o)))!=s(o),plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,plus(o,s(o)))!=plus(o,s(plus(o,o))))Stk: ()Act0: (plus(A,s(B))=s(plus(A,B)))Act1: ((A=B=>(C=D=>plus(A,C)=plus(B,D))))Act2: ((s(A)=s(B)=>A=B))Act3: (A=A)Act4: ((A=B=>B=A))Act5: ((A=B=>(C=A=>C=B)))======================================(6, 0)>>> step(0)action 0Cla: (s(plus(o,plus(o,o)))!=s(o))Path: (plus(o,s(plus(o,o)))!=s(o),plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,s(plus(o,o)))!=s(plus(o,plus(o,o))),plus(o,plus(o,s(o)))!=plus(o,s(plus(o,o))))Stk: ()Act0: ((A=B=>s(A)=s(B)))Act1: ((s(A)=s(B)=>A=B))Act2: ((A=B=>B=A))Act3: ((A=B=>(C=A=>C=B)))======================================(4, 0)>>> step(0)action 0Cla: (plus(o,plus(o,o))!=o)Path: (s(plus(o,plus(o,o)))!=s(o),plus(o,s(plus(o,o)))!=s(o),plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,s(plus(o,o)))!=s(plus(o,plus(o,o))),plus(o,plus(o,s(o)))!=plus(o,s(plus(o,o))))Stk: ()Act0: ((s(A)=s(B)=>A=B))Act1: ((A=B=>B=A))Act2: ((A=B=>(C=A=>C=B)))======================================(3, 0)>>> step(2)action 2Cla: (plus(o,plus(o,o))!=R,R!=o)Path: (plus(o,plus(o,o))!=o,s(plus(o,plus(o,o)))!=s(o),plus(o,s(plus(o,o)))!=s(o),plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,s(plus(o,o)))!=s(plus(o,plus(o,o))),plus(o,plus(o,s(o)))!=plus(o,s(plus(o,o))))Stk: ()Act0: ((A=B=>(C=D=>plus(A,C)=plus(B,D))))Act1: ((s(A)=s(B)=>A=B))Act2: (A=A)Act3: ((A=B=>B=A))Act4: ((A=B=>(C=A=>C=B)))======================================(5, 0)>>> step(0)action 0Cla: (plus(o,o)!=X,o!=V)Path: (plus(o,plus(o,o))!=plus(V,X),plus(o,plus(o,o))!=o,s(plus(o,plus(o,o)))!=s(o),plus(o,s(plus(o,o)))!=s(o),plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,s(plus(o,o)))!=s(plus(o,plus(o,o))),plus(o,plus(o,s(o)))!=plus(o,s(plus(o,o))))Stk: (plus(V,X)!=o)Act0: (plus(A,o)=A)Act1: ((A=B=>(C=D=>plus(A,C)=plus(B,D))))Act2: ((s(A)=s(B)=>A=B))Act3: (A=A)Act4: ((A=B=>B=A))Act5: ((A=B=>(C=A=>C=B)))======================================(6, 0)>>> step(0)action 0Cla: (o!=V)Path: (plus(o,plus(o,o))!=plus(V,o),plus(o,plus(o,o))!=o,s(plus(o,plus(o,o)))!=s(o),plus(o,s(plus(o,o)))!=s(o),plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,o)!=o,plus(o,s(plus(o,o)))!=s(plus(o,plus(o,o))),plus(o,plus(o,s(o)))!=plus(o,s(plus(o,o))))Stk: (plus(V,o)!=o)Act0: ((s(A)=s(B)=>A=B))Act1: (A=A)Act2: ((A=B=>B=A))Act3: ((A=B=>(C=A=>C=B)))======================================(4, 0)>>> step(1)action 1Cla: (plus(o,o)!=o)Path: (plus(o,plus(o,o))!=o,s(plus(o,plus(o,o)))!=s(o),plus(o,s(plus(o,o)))!=s(o),plus(o,plus(o,s(o)))!=s(o),'#')Lem: (plus(o,plus(o,o))!=plus(o,o),plus(o,s(plus(o,o)))!=s(plus(o,plus(o,o))),plus(o,plus(o,s(o)))!=plus(o,s(plus(o,o))))Stk: ()Act0: (plus(A,o)=A)Act1: ((s(A)=s(B)=>A=B))Act2: ((A=B=>B=A))Act3: ((A=B=>(C=A=>C=B)))======================================(4, 0)>>> step(0)action 0Cla: ()Path: ()Lem: ('#')Stk: ()======================================(0, 1)>>>
Major failure patterns
Major failure patterns
The dominant failure pattern in Stage 3 is that the trained system tends to overuse equality congruence axioms. I.e. when trying to prove A + B = C +D or A x B = C x D, it proceeds by reducing the problem to proving A = C and B = D, which does not work in general. In the training set, all numbers are 0 and 1 and such a heuristic approach works more often. Using congruence axioms in these situations is risky, but when it leads to a successful proof, it yields shorter proof. We illustrate this below by showing a safer and a riskier proof of problem (1+1) x 1 = 2 x 1, as well as a failed proof attempt of the problem (1+1) x 1 = 1 x 2, where congruence should not have been applied.
Proof of (1+1) x 1 = 2 x 1 in 33 steps using a safer, more conservative approach
Proof of (1+1) x 1 = 2 x 1 in 33 steps using a safer, more conservative approach
The problem is proven by first calculating the value of the right side ((1+1) x 1) and then calculating the left side (2 x 1). This strategy generalizes to other numbers, but the resulting proof is rather long.
Proof of (1+1) x 1 = 2 x 1 in 8 steps using a risky, heuristic approach
Proof of (1+1) x 1 = 2 x 1 in 8 steps using a risky, heuristic approach
The problem is reduced to proving 1+1 = 2 and 1=1. This results in a short proof, but the strategy does not generalize to other numbers.
Failed proof attempt of the problem (1+1) x 1 = 1 x 2
Failed proof attempt of the problem (1+1) x 1 = 1 x 2
The proof proceeds like the previous, but here the appliation of the congruence axiom is not valid: the problem is reduced to proving 1+1 = 1 and 1=2, which obviously fails.
Axioms of Robinson Arithmetic using unary encoding of numbers
Axioms of Robinson Arithmetic using unary encoding of numbers
Robinson Arithmetic defines basic properties of arithmetic expressions on the nonnegative integers. The signature of the language contains atom 'o' (representing 0), functions 's', 'plus' and 'mul' (for +1, + and x, respectively), and the equality predicate '='. For example, formula 2 x 1 + 1 = 3 + 0 is written as plus(mul(s(s(o)), s(o)), s(o)) = plus(s(s(s(o))), o). The total number of actions if 24.
%theorem: mul(1,1) = 1
fof(zeroSuccessor,axiom, ! [X]: (o != s(X))).
fof(differentSuccessors,axiom, ! [X,Y]: (s(X) != s(Y) | X = Y)).
fof(additionZero,axiom, ! [X]: (plus(X,o) = X)).
fof(additionSuccessor,axiom, ! [X,Y]: (plus(X,s(Y)) = s(plus(X,Y)))).
fof(multiplicationZero,axiom, ! [X]: (mul(X,o) = o)).
fof(multiplicationSuccessor,axiom, ! [X,Y]: (mul(X,s(Y)) = plus(mul(X,Y),X))).
fof(myformula, conjecture, mul(s(o),s(o)) = s(o)).
Axioms of Robinson Arithmetic using binary encoding of numbers
Axioms of Robinson Arithmetic using binary encoding of numbers
Term b(X, Y) represents X + 2Y, i.e., 10 is represented as term b(0,b(1,b(0,1))). This makes the domain theory somewhat more complex: the number of axioms increases from 6 to 17 and the number of actions increases from 24 to 40. However, the representation of terms is logarithmically shorter.
%theorem: mul(n1,n1) = n1
fof(zeroSuccessor,axiom, ! [X, Y]: (n0 != b(X, Y))).
fof(oneSuccessor,axiom, ! [X, Y]: (n1 != b(X, Y))).
fof(differentSuccessors,axiom, ! [X1, Y1, X2, Y2]: (b(X1, Y1) != b(X2, Y2) | (X1 = X2 & Y1 = Y2))).
fof(predecessor, axiom, ! [X]: (X = n0 | X = n1 | ? [Y,Z]: b(Y,Z) = X)).
fof(additionZero,axiom, ! [X]: (plus(X, n0) = X)).
fof(additionOnen1,axiom, plus(n0, n1) = n1).
fof(additionOne2,axiom, plus(n1, n1) = b(n0,n1)).
fof(additionOne3,axiom, ! [X]: (plus(b(n0,X),n1) = b(n1,X))).
fof(additionOne4,axiom, ! [X]: (plus(b(n1,X),n1) = b(n0,plus(X,n1)))).
fof(additionMoren1,axiom, ! [X,Y]: (plus(n0,b(X,Y)) = b(X,Y))).
fof(additionMore2,axiom, ! [X,Y]: (plus(n1,b(X,Y)) = plus(b(X,Y), n1))).
fof(additionMore2,axiom, ! [X1,Y1,X2,Y2]: (plus(b(X1,Y1),b(X2,Y2)) = plus(b(X1,plus(Y1,Y2)),X2))).
fof(multiplicationZeron1,axiom, ! [X]: (mul(X,n0) = n0)).
fof(multiplicationZero2,axiom, ! [X]: (mul(n0,X) = n0)).
fof(multiplicationOnen1,axiom, ! [X]: (mul(X,n1) = X)).
fof(multiplicationOne2,axiom, ! [X]: (mul(n1,X) = X)).
fof(multiplicationMore,axiom, ! [X1, Y1, X2, Y2]: (mul(b(X1, Y1), b(X2, Y2)) = plus(plus(plus(b(n0,b(n0,mul(Y1, Y2))), b(n0, mul(Y1, X2))), b(n0, mul(X1, Y2))), mul(X1, X2)))).
fof(myformula, conjecture, mul(n1,n1) = n1).
Google Sites
Report abuse