Editing Larch Prover (section)

{{short description|Interactive theorem proving system}}
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 [[electrical network|circuits]], concurrent [[algorithm]]s, hardware, and software.<ref>[https://www.cs.cmu.edu/afs/cs.cmu.edu/project/larch/www/survey.txt 1985 Larch survey, Çarnegie Mellon University]</ref>  

Unlike most theorem provers, which attempt to find [[Mathematical proof|proof]]s automatically for correctly stated conjectures, LP was intended to assist users in finding and correcting flaws in conjectures&mdash;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.