Larch Prover

The Larch Prover, or LP for short, is an interactive theorem proving system for multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990s to reason about designs for circuits, concurrent algorithms, hardware, and software.
Unlike most theorem provers, which attempt to find proofs automatically for correctly stated conjectures, LP was intended to assist users in finding and correcting flaws in conjectures—the predominant activity in the early stages of the design process. It worked efficiently on large problems, had many important user amenities, and could be used by relatively naïve users.

Development

LP was developed by Stephen Garland and John Guttag at the MIT Laboratory for Computer Science with assistance from James Horning and James Saxe at the DEC Systems Research Center, as part of the Larch project on formal specifications. It extended the REVE 2 equational term rewriting system developed by Pierre Lescanne, Randy Forgaard with assistance from David Detlefs and Katherine Yelick. It supports proofs by equational term rewriting, cases, contradiction, induction, generalization, and specialization.
LP was written in the CLU programming language.

Sample LP Axiomatization


declare sorts E, S
declare variables e, e1, e2: E, x, y, z: S
declare operators
 : -> S
 : E -> S
 insert: E, S -> S
 __ \union __: S, S -> S
 __ \in __: E, S -> Bool
 __ \subseteq __: S, S -> Bool
 ..
set name setAxioms
assert
 sort S generated by, insert;
 = insert;
 ~;
 e \in insert <=> e = e1 \/ e \in x;
 \subseteq x;
 insert \subseteq y <=> e \in y /\ x \subseteq y;
 e \in <=> e \in x \/ e \in y
 ..
set name extensionality
assert \A e => x = y

Sample LP Proofs


set name setTheorems
prove e \in 
qed
prove \E x \A e 
 resume by specializing x to insert
qed
% Three theorems about union 
prove x \union = x
 instantiate y by x \union in extensionality
qed
prove x \union insert = insert
 resume by contradiction
 set name lemma
 critical-pairs *Hyp with extensionality
qed
prove ac \union
 resume by contradiction
 set name lemma
 critical-pairs *Hyp with extensionality
 resume by contradiction
 set name lemma
 critical-pairs *Hyp with extensionality
qed
% Three theorems about subset
set proof-methods =>, normalization
prove e \in x /\ x \subseteq y => e \in y by induction on x
 resume by case ec = e1c
 set name lemma
 complete
qed
prove x \subseteq y /\ y \subseteq x => x = y
 set name lemma
 prove e \in xc <=> e \in yc by <=>
 complete
 complete
 instantiate x by xc, y by yc in extensionality
qed
prove \subseteq z <=> x \subseteq z /\ y \subseteq z by induction on x
qed
% An alternate induction rule
prove sort S generated by,, \union
 set name lemma
 resume by induction
 critical-pairs *GenHyp with *GenHyp
 critical-pairs *InductHyp with lemma
qed