git @ Cat's Eye Technologies Eqthy / d5f734f
Rewrite part of README for clarity, giving the rules of inference. Chris Pressey 2 years ago
1 changed file(s) with 27 addition(s) and 13 deletion(s). Raw diff Collapse all Expand all
+27
-13
README.md less more
00 Eqthy
11 =====
22
3 **Eqthy** is a language for equational proofs. It's similar to, but different from, the "calculational style"
4 developed and popularized by Dijkstra et al.
3 **Eqthy** is a language for equational proofs. It's similar to, but
4 different from, the "calculational style" developed and popularized by
5 Dijkstra et al.
56
6 This document is a sketch. It describes the language. It mentions some things a processor of the language
7 might be expected to do.
7 This document is a sketch. It describes the language. It mentions some
8 things a processor of the language might be expected to do.
89
9 An Eqthy development consists of any number of axioms and theorems. Each axiom is an equation.
10 An equation equates two terms. Terms consist of constructors (also called function symbols)
11 and variables. Variables begin with uppercase letters. Constructors begin with lowercase
12 letters are followed by a list of zero or more subterms, enclosed in parentheses.
13 If a term has no subterms, it is called an "atom" and the parentheses may be omitted.
10 An Eqthy development consists of any number of axioms and theorems. Each
11 axiom is an equation. An equation equates two terms. Terms consist of
12 constructors (also called function symbols) and variables. Variables begin
13 with uppercase letters. Constructors begin with lowercase letters are
14 followed by a list of zero or more subterms, enclosed in parentheses. If a
15 term has no subterms, it is called an "atom" and the parentheses may be
16 omitted.
1417
1518 Each axiom may optionally by named. Here are some example axioms:
1619
1821 axiom (#id-left) mul(e, A) = A
1922 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
2023
21 A theorem gives an equation, followed by a sequence of equations that shows that the
22 validitiy of the equation follows from the axioms and theorems previously given in
23 the Eqthy souce. Each equation in the sequence is optionally followed by a hint,
24 indicating what rule was used to derive it.
24 A theorem gives an equation, followed by a sequence of equations that shows
25 that the equation can be derived using the available means. The available
26 means are:
27
28 * the axioms that have been previously defined
29 * the theorems that have been previously proved
30 * the rules of inference of equational logic, which are
31 * Reflexivity (A=A)
32 * Transitivity (if A=B and B=C then A=C)
33 * Substitution (if x(A)=y(A) then x(B)=y(B))
34 * Congruence (if A=B then x(A)=x(B))
35
36 The sequence of equations following a theorem is a proof. Each equation in
37 the proof is optionally annotated with a hint that follows it, indicating what
38 axiom, theorem, or rule of inference was used to derive it.
2539
2640 theorem (#id-comm)
2741 mul(A, e) = mul(e, A)