A logical language for theorem proving and geometry solving
May 6, 2024 (last updated May 15, 2024)
The following is a brief and high-level summary of a logical language that is suitable as input to a theorem prover for geometry solving, e.g. Meringue.
A logical form language
The input to the theorem prover is a script written in a logical form language [L16]. By logical form language, we mean something very much like a logic programming language, i.e. a language based on Horn clauses with equality and uninterpreted functions, except that there is more emphasis on the logical and less on the extra-logical programming parts, e.g. cut or non-pure I/O.
For example, the lines:
axm for a, b, c the abc {
triangle(a, b, c) -> abc :- -/collinear(a, b, c)
}
define a logical rule that may be translated into the following natural language sentence: “Suppose that $a$, $b$, and $c$ are not collinear. Then, $a$, $b$, and $c$ form a triangle $abc$.”
In the line above,
a, b, and
c are universally quantified bound variables,
abc is a functionally bound variable,
and triangle and collinear are
free or global variables.
The terms triangle(a, b, c) -> abc and
-/collinear(a, b, c) are logical tuples
representing logical propositions.
Following the Prolog convention, the arrow :-
symbolizes right-to-left inference: given the conditions
on the right-hand-side of the arrow, the conclusion on the
left-hand-side follows.
(Alternatively, the left-to-right arrow -:
would also work analogously.)
The logical negation -/ simply follows
the rule of first-degree entailment
[AB63],
rather than the stratified negation-as-failure
usually seen in logic programming.
The keyword axm, which begins the definition
of the rule, is rather arbitrary;
other possible keywords include thm,
lem, rule, etc.
The free variables
triangle and
collinear above refer to logical relations,
which must be defined prior to their use in a logical rule.
Sensible definitions would be the two lines:
symm fun triangle/3+1 symm rel collinear/3
The
triangle functional relation has a
functional arity of 3+1, i.e. it is a function
of a 3-tuple argument returning exactly 1 output.
The collinear relation simply has a 3-tuple
argument.
The keyword symm marks both relations as
symmetric relations, a light syntactic sugar that auto-defines
logical rules to generate all permutations of their 3-tuple
arguments.
Propositional facts may be declared using standard keywords, e.g.
let ABC <- triangle(A, B, C) or
where -/collinear(A, B, C).
Proof goals may be specified with a special keyword,
e.g. propose.
Language extensions
The logical form language we described above is sufficient for encoding most olympiad-style geometry problems, which correspond to fixed-point saturation of pure (side-effect-free) logical rules, interpreted with choice of functional applications. One might also describe such a fragment as logically monotonic [HA19]; that is, additional logical deductions strictly increase knowledge without refuting what is already known.
For more general domains, it makes sense to carve out alternatives along each of the pure/functional-choice axes of our logic.
Whereas pure logical rules are sufficient for geometry, non-pure (or side-effect-ful) logical rules may be necessary for describing general domains. Just as a pure logical rule is defined with the help of the
:- or -: arrows,
a non-pure logical rule may be defined by the arrows
:~ (right-to-left non-pure rule) or
~: (left-to-right non-pure rule).
Non-pure logical rules additionally may also introduce non-pure logical destruction
~/
on the conclusion side of the rule,
which removes a logical tuple argument.
Even more generally, a non-pure imperative effect may be introduced with the
!
(read: “bang”) operator.
(In Prolog, the bang operator is typically used for
cut, but we are not here to reproduce Prolog.)
Imperative effects are, most generally, opaque and
sequential (i.e. non-monotonic).
A functional choice as used for geometric constructions may be generalized to a top-level choice. Any top-level (pure or non-pure) logical rule may be marked
choose to exempt it from fixed-point
saturation and to instead interpret it during the
evaluation-of-choices phase.
References
[AB63] A. R. Anderson and N. D. Belnap, Jr. “First Degree Entailments.” Math. Annalen 149, pp. 302-319 (1963).
[HA19] Joseph M. Hellerstein and Peter Alvaro. “Keeping CALM: When Distributed Consensus is Easy.” arXiv preprint 1901.01930v2 (2019).
[L16] Percy Liang. “Learning Executable Semantic Parsers for Natural Language Understanding.” Communications of the ACM 59(9), pp. 68-76 (2016).