A Rational Reconstruction of a System for

Experimental Mathematics

Jacques Carette1 , William M. Farmer1 , and Volker Sorge2

1
Department of Computing and Software
McMaster University, Hamilton, Ontario, Canada
{carette,wmfarmer}@mcmaster.ca
http://www.cas.mcmaster.ca{carette,wmfarmer}
2
School of Computer Science, University of Birmingham, UK,
V.Sorge@cs.bham.ac.uk, http://www.cs.bham.ac.uk/vxs

Abstract. In previous papers we described the implementation of a sys-

tem which combines mathematical object generation, transformation and
filtering, conjecture generation, proving and disproving for mathemati-
cal discovery in non-associative algebra. While the system has generated
novel, fully verified theorems, their construction involved a lot of ad hoc
communication between disparate systems. In this paper we carefully
reconstruct a specification of a sub-process of the original system in a
framework for trustable communication between mathematics systems
put forth by us. It employs the concept of biform theories that enables
the combined formalisation of the axiomatic and algorithmic theories
behind the generation process. This allows us to gain a much better
understanding of the original system, and exposes clear generalisation
opportunities.

1 Introduction
Over the last decade several environments and formalisms for the combination
and integration of mathematical software systems [2, 15] have been proposed.
Many of these systems aim at a traditional automated theorem proving ap-
proach, in which a given conjecture is to be proved or refuted by the cooperation
of different reasoning engines. However, they offer little support for experimental
mathematics in which new conjectures are constructed by an interleaved process
of model computation, model inspection, property conjecture and verification.
And while for example the Theorema system [4] supports many of these ac-
tivities, there are currently no systems available that provide, in an easy to use
environment, the flexible combination of diverse reasoning systems in a plug-and-
play fashion via a high level specification of experiments, despite some previous
research in that direction [1, 3].
[8, 14] presents an integration of more than a dozen different reasoning systems
first order theorem provers, SAT solvers, SMT solvers, model generators, com-
puter algebra, and machine learning systemsin a general bootstrapping algo-
rithm to generate novel theorems in the specialised algebraic domain of quasi-
groups and loops. While the integration leads to provably correct results, the
2 Carette, Farmer, Sorge

integration itself was achieved in an ad-hoc manner, i.e., systems were combined
and recombined in an experimental fashion with a set of custom-built bridges
that not only perform syntax translations but also certain filtering functions.
In this paper we report on a rational reconstruction of an interesting sub-
process of the bootstrapping algorithm, namely the generation of isotopy in-
variants (presented in Sec. 2), using the framework for trustable communication
between mathematics systems that was put forth in [6]. It employs the con-
cept of biform theories (Sec. 3) that enables the combined formalisation of the
axiomatic and algorithmic theories behind the generation process. It turns out
that it is surprisingly difficult to separate the syntactic, semantic, and algorith-
mic level of the current implementation. We present the formalisation in terms
of the necessary semantic and syntactic concepts in Sec. 4 and of biform theories
describing the actual computations in Sec. 5. The aim of this work is to expose
the general principles behind the combination and communications of the single
systems. It is currently only a purely theoretical reconstruction of the current
implementation, and we do not have or even plan an implementation of the pro-
cess in the framework of biform theories. However, the work should ultimately be
used in the design of a flexible environment for experimental mathematics that
enables a user to specify complex experiments on a high level without the need
of detailed knowledge of the underlying logical relations and the particularities
of the integrated systems.
Note that, as in [6], we abstract out the details of the idiosyncratic syntax
of each of the systems. We use a uniform abstract syntax (in this case, we need
4 separate languages, each embedded in the other) for the specification. This
allows us to abstract out the tedious engineering of transformations in and out
of the actual systems. On the other hand, any transformation beyond trivial
parsing and pretty-printing is explicitly specified.
The specification we present involves (at least) 3 levels of mathematical dis-
course: using the language of mathematics, we are specifying (syntactically) the
semantics of a computer system which manipulates (the syntax of) mathematical
theories, which are themselves inhabited by mathematical objects represented
syntactically. Each level also possesses semantic models, which is ultimately what
we want, but for computer manipulation, must be handled syntactically. Sepa-
rating these languages cleanly is a difficult task as the reader will soon witness.

2 Problem

The particular problem we are concerned with is the process of generating isotopy
invariants for loops, which is part of the overall classification procedure presented
in [14]. We give a brief, high level description of the procedure here. The more
formal, mathematical details and definitions are presented in Sec. 4.
A loop is a quasigroup with identity, i.e., an algebraic structure (L, ) sat-
isfying the following two axioms: a, b. (x.x a = b) (y.a y = b) and
x.x e = e x = x. We say two loops (L, ) and (M, ) are isotopic to each
otheror L is an isotope of M if there are bijective mappings , , from
 Rational Reconstruction 3

L to M such that, for all x, y L, (x) (y) = (x y) holds. A property

P , that is preserved under the isotopy mapping (i.e., if P holds for L then it
also holds for all its isotopes) is called an isotopy invariant. In our approach we
generate universal identities, a particular type of isotopy invariants, presented
by Falconer [9]. To find universal identities we have implemented the procedure
presented in Fig 1.
The basic idea of our procedure Generate Equations
is to find identities (i.e., universally (LISP)

quantified equations) that hold for

some loop, by first generating iden-
tities and then checking, which iden- Mace Mace Mace
tity has a non-trivial loop satisfy-
ing it, using a model generator. All If Loops of order
at most 8 exist
identities for which a loop exists are
then transformed into derived identi- Generate Universal Identity
ties (see Sec. 4 Def. 6). All derived (LISP)
identities for which we can prove, by
means of a first order automated the-
orem prover, that they are invariant Vampire Vampire EProver EProver
under isotopy are universal identities.
Note that, for each universal identity,
If UID is
we show that it is an invariant under isotopy invariant

isotopy independently of the size of

a loop. We can therefore reuse these Set of
universal identities in different clas- Isotopy
Invariants
sifications. Consequently, we collect
universal identities in a pool of con-
firmed isotopy invariants, which we
use in the overall bootstrapping al- Finder Finder Finder
gorithm. That is, during the classi-
If Loops of
fication of loops of a particular size order n exists

n, we draw on the pool of invari-

ants by first filtering them again using Isotopy
another model generator to generate Invariants
to attempt
loops of size n that satisfy the invari-
ant. We then extract those invariants
for which at least one loop of order n Bootstrapping Algorithm
exists, and we use only these as poten-
tial discriminants. Note that the filter Fig. 1. Current implementation.
discards any invariants which cannot solve any discrimination problem, as no
loop of size n satisfies the invariant property.
So far we have generated and verified 8, 530 isotopy invariants. These have
been employed as one means, among others, to generate two novel classifications
for loops of order 6 and 7 with respect to isomorphism. Observe, that we currently
concentrate only on the subprocess for generating isotopy invariants and that
4 Carette, Farmer, Sorge

the general bootstrapping algorithm is not the subject of the paper. For more
details and results of the classification of quasigroups and loops with respect to
both isomorphism and isotopism we refer the reader to [8, 14].

3 Biform Theories

The notion of a biform theory was introduced in [13] as the basis for ffmm,
a Formal Framework for Managing Mathematics. Informally, a biform theory
is simultaneously an axiomatic and an algorithmic theory. We present here a
formulation of a biform theory that is simpler than the one given in [13].

General Logics A general language is a pair L = (E, F ) where E is a set of

syntactic entities called the expressions of L and F E is a set of expressions
called the formulas of L. For example, if F is a first order language, then LF =
(T F, F ) is a general language where T and F are the sets of terms and
formulas of F , respectively. In the rest of this paper, let L = (E, F ) be a general
language.
A general logic is a set of general languages with a notion of logical conse-
quence. In the rest of this paper, let K be a general logic. L is a language of K
if it is one of the general languages of K. If L is a language of K and {A}
is a set of formulas of L, then |=K A means A is a logical consequence of
in K. For example, let FOL be a general logic representation of first order logic
such that L is a language of FOL iff L = LF for some first order language F
and |=FOL A means A is a logical consequence of in first order logic.
An axiomatic theory in K is a pair T = (L, ) where L = (E, F ) is a language
of K and F. L is the language of T , and is the set of axioms of T . A
formula A of L is a logical consequence of T if |=K A.

Transformers For n 0, an n-ary transformer in L is a pair = (, )

where is a symbol and is an algorithm that implements a (possibly partial)
function f : E n E. The symbol serves as a name for the algorithm . There
is no restriction on how the algorithm is presented. For example, it could be a a
-expression in L or a program written in Lisp or Haskell (or even C or Java).
Let dom() denote the domain of , i.e., the subset of E n on which f is
defined. Suppose E1 , . . . , En are expressions in E. If (E1 , . . . , En ) dom(),
the expression (E1 , . . . , En ) denotes the output of when given E1 , . . . , En as
input, i.e., it denotes f (E1 , . . . , En ) E (and is thus defined ). If (E1 , . . . , En ) 6
dom(), (E1 , . . . , En ) does not denote anything (and is thus undefined ). The
expression (E1 , . . . , En ) is not required to be in E; it will usually be an expres-
sion of the metalanguage of L but not of L itself.

Example 1. Suppose LF = {EF , FF } is the general language corresponding to a

first order language F . Let = (,
) be a unary transformer in LF such that:

1. (E) is defined iff E FF .

 Rational Reconstruction 5

2. If (A) is defined, it denotes a formula B FF that is in prenex normal

form and is logically equivalent to A.
That is, the algorithm
transforms any formula of LF into a logically equivalent
formula in prenex normal form. The expression (E) cannot be an expression
in LF (without some mechanism, such as Godel numbering, for formalising the
syntax of LF in LF itself). 2
Example 2. Suppose LF = {EF , FF } is again the general language corresponding
to a first order language F . Let = (,
) be a ternary transformer in LF such
that:
1. (E1 , E2 , E3 ) is defined iff E1 is a term of F , E2 is a variable of F , and E3
is a formula of F .
2. If (t, x, A) is defined, it denotes the result of simultaneously substituting t
for each free occurrence of x in A.
That is, given t, x, A, the algorithm
transforms the formula A into the formula
A[x 7 t]. Again the expression (E1 , E2 , E3 ) cannot be an expression in EF . 2
Example 3. Let STT be a general logic representation of simple type theory.
Suppose T = (L, ) is an axiomatic theory of a complete ordered field in STT
and that we have defined in T a type real of real numbers and the basic concepts
of calculus such as limits, continuity, derivatives, etc. Let = (,
) be a unary
transformer in L such that:
1. (E) is defined iff E is an expression of L of type real real.
2. If (E) is defined, it is an expression of L of type real real that denotes
the derivative of the function denoted by E.
That is,
is an algorithm that differentiates expressions that denote functions
on the real numbers. 2
An algorithmic theory is a pair T = (L, ) where L is a general language
and is a set of transformers in L. L is called the language of T , and is the
set of algorithms of T . For more on transformers, see [12, 13].

Rules A rule in L is a pair R = (, M ) where:

1. = (, ) is an n-ary transformer in L.
2. M is a formula that uses to relate the values of the inputs to
to the
value of the output of .
The transformer of R, written trans(R), is , and the meaning formula of R,
written mean(R), is M . The meaning formula M , which specifies the semantic
relationship between the tuple of inputs and the output of the algorithm ,
will usually be an expression of the metalanguage of L but not of L itself. For
each n-tuple I = (E1 , . . . , En ) of inputs to
, we assume that M reduces to
a formula MI of L which is called the instance of M with respect to I. An
instance of M specifies the relationship between the values of a given tuple of
6 Carette, Farmer, Sorge

input expressions and the value of the resulting output expression. Let inst(R)
be the set of instances of M . M can often be conveniently expressed as a formula
schema.
Example 4. Let R = (, M ) where:
1. = (,
) is the transformer in LF given in Example 1.
2. M is the formula schema A (A) where A is a formula of LF .
If A is the formula p(c) x.q(x) (where c is a constant) and the result of
applying to (A) is x.p(c) q(x), then (p(c) x.q(x)) (x.p(c) q(x)) is
the instance of M with respect to (A). 2
Example 5. Let R = (, M ) where:
1. = (, ) is the transformer in LF given in Example 2.
2. M is the formula schema (x = t A) (t, x, A) where t is a term, x is a
variable, and A is a formula of LF and t is free for x in A.
If t is a term, x is a variable, and A is f (x, y) = g(x), then (x = t f (x, y) =
g(x)) f (t, y) = g(t) is the instance of M with respect to (t, x, A). 2
Example 6. Let R = (, M ) where:
1. = (, ) is the transformer in the language L of the theory T given in
Example 3.
2. M is the formula schema derivative(E) = (E) where E is of type real real.
derivative is an expression of L of type (real real) (real real) that
maps a function to its derivative. M thus asserts that the derivative of the
function denoted by E is the function denoted by (E).
If E is x : real.x2 , then derivative(x : real.x2 ) = (x : real.2 x) is the instance of
M with respect to (E). 2
For the sake of convenience, we will view a formula A of L as a (transformer-
less) rule in L and assume that trans(A) is undefined, mean(A) = A, and
inst(A) = {A}.

Biform Theories A biform theory in K is a pair T = (L, ) where L is a

language of K and is a set of rules in L. ( may include formulas of L viewed
as transformer-less rules.) L is the language of T , and is the set of axioms of
T.
T can be viewed as simultaneously both an axiomatic theory and an algorith-
mic theory. TheS axiomatic theory of T is the axiomatic theory Taxm = (L, ) in
K where = R inst(R), while the algorithmic theory of T is the algorithmic
theory Talg = (L, ) where = {trans(R) | R and trans(R) is defined}.
The axioms of T which are formulas and rulesare the background as-
sumptions of T in an implicit form. The axioms of Taxm which are formulas
aloneare the background assumptions of T in an explicit form. A rule R in
L is a logical consequence of T if, for all formulas A inst(R), A is a logical
consequence of Taxm . Thus, the axioms of T are trivially logical consequences of
T . Notice also that, since we are assuming that the formulas of L are rules in L,
every logical consequence of Taxm is also a logical consequence of T .
 Rational Reconstruction 7

4 Definitions

We now render the problem from Sec 2 precisely by giving the relevant formal
definitions. To facilitate the formal specification as biform theories in Sec 5 we
painstakingly distinguish between the semantics of the mathematical concepts,
the languages necessary to express them, and the purely syntactic expression.

4.1 Semantic Concepts

Definition 1 A loop is a non-empty set G together with a binary operation

and a distinguished element e G such that

a, b G. (x G.x a = b) (y G.a y = b) and x G.x e = e x = x.

Definition 2 Let G be a loop with binary operation , then we can define two
additional binary operations / and \ by
1. x, y G.x (x\y) = y and x, y G.x\(x y) = y
2. x, y G.(y/x) x = y and x, y G.(y x)/x = y
Definition 3 Let G, H be two loops with respective binary operation and .
We say G is isotopic to H if there are bijective mappings , , from G to H
such that for all x, y G, (x) (y) = (x y) holds.
Definition 4 Let G be a loop and let P be a property that holds for G. We call
P an isotopy invariant if P is preserved under the isotopy mapping (i.e., if P
holds for G than it also holds for all its isotopes).
Definition 5 Let G be a loop with binary operation . w is a word of G if it is a
combination of elements of G with respect to the loop operation . Let w1 , w2 be
two words in G, then w1 = w2 defines a loop identity if it holds for all elements
of G.
Definition 6 Let G be a loop with binary operations , \, /. Given a word w in
G, we define its corresponding derived word w by
1. if w = x, x G, then w = x;
2. if w = u v, then w = (u/y) (z\v), where u, v, y, z G.
Given a loop identity w1 = w2 of G, we define its corresponding derived identity
as w1 = w2 .
Definition 7 Let G be a loop with binary operations , \, / and w1 = w2 be a
derived identity in G. Then w1 = w2 is a universal identity if it is an isotopy
invariant.

4.2 Languages

In order to express the definitions of the syntactic concepts we give the necessary
languages by stepwise extending the basic language of first order logic with
equality (FOL+EQ). This will later enable us to define biform theories with
minimal languages. Generally, we need a fair bit more machinery to define our
various meaning functions; thus we will freely use Simple Type Theory (STT)
[7, 10] as our general environment.
8 Carette, Farmer, Sorge

As a general typographical convention, we will underline all the symbols when

we refer to the syntactic version of a symbol we already have in our semantics.
We will not however underline variables, to ease (somewhat) the readability of
the results. We assume that the reader is proficient enough in FOL+EQ and
STT so that we do not need to repeat their syntactic definition here.
We first extend FOL+EQ to the language Loop by adding a binary function
and a constant e. In a next step we add the two binary operations \ and /
to Loop to obtain Loop . In fact, in Loop , we need two loops, so we in fact
add e1 , 1 , \1 , /1 and e2 , 2 , \2 , /2 to Loop . While these languages are sufficient
to express the syntactic objects manipulated during the computation, we also
need to express the meaning formulas for transformers in the language of a
biform theory. This will necessarily be (at least) a second order logic, as we are
quantifying over loops. It also is much easier to specify if we have access to a bit
more machinery, such as lambda expressions and unique choice. We therefore
use STT, as a superset of Loop , for this purpose. Thus altogether we have the
following sequence of languages: FOL+EQ Loop Loop STT

4.3 Syntactic Concepts

Let V be a set of variables, with xi V. Let y, z be two new symbols not in V
and let V = V {z, y}.
Word ::= xi | e | Word Word
Identity ::= x.Word = Word
Word ::= xi | e | (Word \ y) (z / Word )
DerivedIdentity ::= x.Word = Word
A Word is a word in the language of loops, composed of variables, an identity
element e and an operation , where all variables of V are understood to
be universally quantified. A Word is a word in the extended language of loops,
composed of variables, and identity element, operation and two new operators,
/ and \, where again variables (V ) are universally quantified. Then Identity and
DerivedIdentity are identities over the respective languages.
We also need syntactic representations of various axioms. For example, we
have that
CircAxm = a, b. (x.xa = b)(y.xy = b) in Loop.
IdAxm = (x.xe = x)(x.ex = x) in Loop.
DivLAxm = (x, y.x(x \ y) = y)(x, y.x \ (xy) = y) in Loop
DivRAxm = (x, y.(y / x)x = y)(x, y.(yx) / x = y) in Loop .
These express respectively the axiom for , the identity e, the left division \ and
the right division /.
Actually, to describe the full semantics, we need two copies of the above,
for two different loops, whose components well naturally denote (e1 , 1 , \1 , /1 )
and (e2 , 2 , \2 , /2 ) respectively. Since we are in STT, we could have easily have
written the above as functions from syntax to syntax, but that would have
 Rational Reconstruction 9

made the presentation too opaque. We also need to represent a finite domain
syntactically. But this essentially amounts to creating n unique names.
We can then continue thus, for all the various concepts defined semantically in
the previous section, which we use syntactically later (like bijective). We should
also define the full syntax for a language of proofs (as the language for the
output of one of our intermediate transformers below), but since the actual
implementation ignores these proofs, it suffices to posit that this language exists.

5 Specification

We can view the generation of isotopy invariants from derived identities and their
selection as possible discriminants for loops of a given size n as a sequence of
single computational processes as displayed in Fig. 2. Each process accomplishes
a different function in the overall computational process, e.g., is a source of
equations, transforms expressions, or filters with respect to different criteria.

Generate Find Rewrite Prove Store Find

Nontrivial Yes
Yes Yes
Equation Equation Invariant Invariant Model
Model of size n
Source Filter Transformation Filter Sink/Source Filter

Fig. 2. Abstract view of the process.

For each module, we have a background (biform) theory that expresses the
language and axioms necessary to describe the rules (and thus the inputs and
outputs) encapsulated in that module. Using appropriate translations and inter-
pretations, we can set up a communication channel (a connection in the language
of [6]). We give detailed formal specifications for each process and their commu-
nications.
We can also give a specification for the global problem for generating uni-
versal identities in general, which corresponds to the dashed box in Fig. 2. This
results in a transformer that operates on a more abstract level. We start by giv-
ing the formal specification for it, before going into the details of the component
processes.
Concretely, for the remainder we let K be the general logic based on STT
as general language. We then define the biform theory for the overall process
consisting as axiomatic theory Taxm = (L, ) and algorithmic theory Talg =
(L, ), where L = STT, contains all axioms defined in 4.1, and contains
one transformer = (, ).

1. () = Generate Universal Identity() is always defined, as it takes no

input. It returns a set of syntactical structures DerivedIdentity, as defined in
Sec. 4.3
10 Carette, Farmer, Sorge

is the implementation of Generate Universal Identity as presented

2.
in [14].
3. M is the meaning formula

U Generate Universal Identity().U DerivedIdentity

Subst(CircAxm, e1 , 1 , \1 , /1 ) Subst(IdAxm, e1 , 1 , \1 , /1 )
Subst(DivLAxm, e1 , 1 , \1 , /1 ) Subst(DivRAxm, e1 , 1 , \1 , /1 )
Subst(CircAxm, e2 , 2 , \2 , /2 ) Subst(IdAxm, e2 , 2 , \2 , /2 )
Subst(DivLAxm, e2 , 2 , \2 , /2 ) Subst(DivRAxm, e2 , 2 , \2 , /2 )
Subst(U, e1 , 1 , \1 , /1 ) , , .bijective() bijective() bijective()
x, y.(x)2 (y) = (x1 y) Subst(U, e2, 2 , \2 , /2 ).

In the formula M the predicate Subst is shorthand for a syntactic replacement

of the symbols e, , , \ / in U by their indexed counterpart to obtain two copies
of loops. This can be implemented similar to the transformer for substitution in
Example 2. However, we omit this level of detail here. Observe also that bijective
is shorthand for the formulas representing the bijectivity property.
For the rest of this section, it is useful to remember that we use for the
name of the function (transformer) while is its implementation. Whenever a
transformer has a more natural name than , we use that name instead.

5.1 Source: Generating Equation

The first step generates a set of identities. The language of the biform theory
is L = Loop and the axiomatic theory is Taxm = (L, {}). We do not need any
axioms as the computation of this module is only a generation of constructs in our
language and, therefore, not based on any logical consequences. In Talg = (L, ),
contains one transformer = (, ).

1. () = Generate Identity() is always defined, as it takes no input. It returns

a set of syntactical structures Identity.
2.
is the implementation of Generate Identity that corresponds to the
grammar given for Identity in Sec. 4.3.
3. M is i Generate Identity.i Identity.
Here M simply states that the elements of the generated set are indeed members
of the syntactic class of identities.

5.2 Filter: Find Non-Trivial Model

The computation defined in this module is more complicated to formalise since

we take a set of identities as input, for each one we try to generate a model of
some specified size, and only output those identities for which we could success-
fully generate a model. Its formalisation can be achieved by using one trans-
former in the context of the other. We have a transformer modelling the general
 Rational Reconstruction 11

computation of a model generator that operates in the context of a transformer

for the particular generation of models of loops satisfying given identities. In
addition this latter transformer performs the actual filtering by discarding those
identities for which no models exist.
The language of the biform theory is Loop and Taxm = (L, ), where con-
tains the axioms given in definition 1. The algorithmic theory Talg contains two
transformers: 1 = (1 , 1 ) specifying the computation of the model genera-
tor and 2 = (2 , 2 ) specifying the filtering operation carried out on a set of
identities.

1. 1 (S, D) = Generate Model(S, D) is defined iff S is a set of syntactic for-

mulas and D is a syntactic representation of the domain. It returns set of
syntactic representation of models if one exists, i.e., for each constant element
in the input a relation in D satisfying E.
2.
1 is the model generation process performed by some integrated model
generator.
3. M is m Generate Model(S, D).(m |= S). Note that m is a model with
interpretations of the symbols of S given as functions represented by sets of
ordered pairs.

Given the transformer for general model generation, we now define the actual
filter operation as:

1. 2 (E, n) = Filter Identities(E, n) is defined iff E is a set of Identity n is

a positive integer. It also returns a set of syntactical structures Identity.
2.
2 is the implementation of Filter Identities that generates the syntactic
representation of the domain of size n given to 1 and applies 1 to each
element in E.
3. M is i Filter Identities(E, n).Generate Model({i}, Dom(n)) 6= .

Observe that in M above Dom(n) is a schema specifying the set of domain

elements computed in Filter Identities, which could itself be specified using
a transformer. Observe also that we have slightly simplified the formalisation,
in that it only takes domains of one size, rather than a range of domain sizes.
We note that both transformers are very general and do not depend on
the particular biform theory they live in. In particular Generate Model works
on any first order language regardless of the language of the biform theory.
Here the theory serves as a way to parameterise the input to the transformer.
Filter Identities performs filtering with respect to model existence. Likewise
it could filter with respect to non-existence of models or return computed models
by interpreting them in the biform theory. Note that Filter Identities is a
total set-to-set function, and the underlying implementation is total as well; even
Generate Model is a total function (it always terminates), however it may return
an empty result1 .
1
In Haskell, we could say that Generate Model belongs in the Maybe Monad.
12 Carette, Farmer, Sorge

5.3 Transformation: Rewrite Equations

This step rewrites loop identities to derived identities. The language of the biform
theory is L = Loop and the axiomatic theory is Taxm = (L, ) where contains
the axioms given in Definitions 1, 2, and 6. In Talg = (L, ), contains one
transformer = (, ).

1. (E) = Generate Derived Identity(E) is defined iff E is a set of Identity.

It returns a set of syntactical structures DerivedIdentity.
2.
is the implementation of the rewrite system given in Def. 6 that performs
syntactic rewriting of an Identity into a DerivedIdentity.
3. M is i E.!d Generate Derived Identity(E). |= i = d.

5.4 Filter: Prove Invariant

Similar to the specification of the filter in Sec. 5.2 this process requires the
combination of two transformers. One for the general proving process and one
that performs the actual filtering.
We define the biform theory for L = STT, with Loop as a distinct sub-
language, Taxm = (L, ), where contains all axioms defined in 4.1, and Talg
containing two transformers: 1 = (1 , 1 ) specifying the computation of the
theorem prover and 2 = (2 , 2 ) specifying the filtering operation.

1. 1 (A, C) = Prove(A, C) is defined iff A is a set of syntactic formulas in

Loop and C is a formula in Loop . It returns a syntactic representation of
a proof if one exists.
2.
2 is the theorem proving process performed by some automated theorem
prover. It takes the elements of A as assumptions and C as a conclusion.
3. M is P roves(Prove(A, C), A C)

Here the predicate P roves checks the correctness of the derivation. The formal-
isation of this predicate depends on the calculus of the integrated prover and
is generally very lengthy to formalise. Since we are not interested in examining
proofs but only their existence at this point, we do not go into any detail here.
Given the transformer for theorem proving, we now define the actual filter
operation as:

1. 2 (E) = Filter Derived Identities(E) is defined iff E is a set of expres-

sions of the form DerivedIdentity. It also returns a set of DerivedIdentity.
2 is the implementation of Filter Derived Identities that generates an
2.
assumption set A from the syntactic representation of the elements of
computes for each element i of E Prove(A, i). It returns a set of all elements
in E for which a proof exists.
3. The meaning function M is of the same form as the meaning function of
the Generate Universal Identity transformer, with the exception that we
now universally quantify over U Filter Derived Identities(E).
 Rational Reconstruction 13

Observe that the Subst is the symbol substitution transformer already used at
the beginning of this section.
The result of this last transformer, the set of syntactic universal identities,
can now be stored for later use. Choosing from this store is again achieved
with a filter that uses model generation, which is similar to the transformer
Filter Identities above. Due to lack of space we omit the detailed formalisa-
tion of these processes here.

6 Conclusions

We have presented a first step towards a rational reconstruction of the classifi-

cation procedure for finite algebras in [8, 14]. The use of biform theories enables
us to express both axiomatic and algorithmic properties of the procedure while
clearly distinguishing syntactic, semantic, and algorithmic levels. Although the
generation of universal identities is only a small sub-process of the overall clas-
sification, its formalisation is surprisingly involved.
This is not really due to the design and current implementation of the al-
gorithm, but rather because some of the operations necessarily intermix syntax
and semantics. Keeping straight what has to be in FOL+EQ, what is safely
in STT, and what is in fact in the meta-language is very difficult. For exam-
ple when generating models with respect to a particular domain, the result is a
semantic entity. Nevertheless, models have to be interpreted as syntax not only
to express the meaning function but also in case the models are used in fur-
ther computations and syntactic manipulations. This also has the effect that the
given domain elements have to be incorporated into the language of the biform
theory, which is currently not possible and subject to future work.
On the other hand, communication between the components is very simple,
since it is all done via FOL+EQ or conservative extensions such as Loop and
Loop . The necessary interpretations [6] between these theories are straightfor-
ward, unlike the more general case where communication occurs amongst more
disparate logics.
The current formalisation already exposes some generalisations. In particular
many of the sub-processes can be expressed as a mixture of computation and
filtering, where the computation is often independent of the particular theory. It
also becomes apparent what is actual input and what has to be specified in the
background theory of a process. This information could be exploited to design
an environment enabling mathematical experimentation by combining systems
on a high level, such that it is only necessary to specify input, output and parts
of the background theory without interaction on the actual logical level.
Our formalisation is certainly not the only possible approach to reconstruct
the generation process. Indeed we could view the entire process as a sequence
of recursive generators and filters. E.g., the first three boxes in Fig. 2 could
be combined in a single transformer that acts as a generator for the next filter.
Comparing different specifications and combinations of transformers for the same
process could expose possible optimisation opportunities for the overall process.
14 Carette, Farmer, Sorge

As we have already discussed, biform theoriesparticularly the meaning for-

mulas of rulesare difficult to formalise in a traditional logic without the means
to reason about syntax. The paper [11] illustrates how biform theories can be
formalised in Chiron, a derivative of von-Neumann-Bernays-Godel (nbg) set
theory that directly supports reasoning about the syntax of expressions. After
an implementation of Chiron is produced, we would like to use Chiron to fully
formalize the work presented in this paper.

References
1. A. Armando and S. Ranise. From integrated reasoning specialists to plug-and-
play reasoning components. In Calmet and Plaza [5], pages 4254.
2. A. Armando and D. Zini. Towards Interoperable Mechanized Reasoning Systems:
the Logic Broker Architecture. In AI*IA Notizie Anno XIII (2000) vol. 3, pages
7075, Parma, Italy, 2000.
3. P. G. Bertoli, J. Calmet, F. Giunchiglia, and K. Homann. Specification and Inte-
gration of Theorem Provers and Computer Algebra Systems. In Calmet and Plaza
[5], pages 94106.
4. B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa,
F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger. Theorema: To-
wards computer-aided mathematical theory exploration. Journal of Applied Logic,
4:470504, 2006.
5. J. Calmet and J. Plaza, editors. Proc. of AISC-98, volume 1476 of LNAI. Springer
Verlag, 1998.
6. J. Carette, W. M. Farmer, and J. Wajs. Trustable communication between math-
ematical systems. In Proc. of Calculemus 2003, pages 5868, 2003.
7. A. Church. A Formulation of the Simple Theory of Types. Journal of Symbolic
Logic, 5:5668, 1940.
8. S. Colton, A. Meier, V. Sorge, and R. McCasland. Automatic generation of clas-
sification theorems for finite algebras. In Proc. of IJCAR 2004, volume 3097 of
LNAI, pages 400414. Springer Verlag, 2004.
9. E. Falconer. Isotopy Invariants in Quasigroups. Transactions of the American
Mathematical Society, 151(2):511526, 1970.
10. W. M. Farmer. STMM: A set theory for mechanized mathematics. J. Autom.
Reasoning, 26(3):269289, 2001.
11. W. M. Farmer. Biform theories in Chiron. In M. Kauers and W. Windsteiger,
editors, Towards Mechanized Mathematical Assistants, LNAI. Springer, 2007 (this
volume).
12. W. M. Farmer and M. von Mohrenschildt. Transformers for symbolic computation
and formal deduction. In S. Colton, U. Martin, and V. Sorge, editors, CADE-17
Workshop on the Role of Automated Deduction in Mathematics, pages 3645, 2000.
13. W. M. Farmer and M. von Mohrenschildt. An overview of a formal framework for
managing mathematics. Annals of Mathematics and Artificial Intelligence, 38:165
191, 2003.
14. V. Sorge, A. Meier, R. McCasland, and S. Colton. Automatic construction and
verification of isotopy invariants. In Proc. of IJCAR 2006, volume 4130 of LNAI,
pages 3651. Springer Verlag, 2006.
15. J. Zimmer and M. Kohlhase. System Description: The MathWeb Software Bus for
Distributed Mathematical Reasoning. In Proc. of CADE-18, 2002.