The third class of proof automaters are the proof assistants, which are guided by humans through the process of generating proofs. The proof assistant's task is to shoulder the burden of the most repetitive and tedious steps in producing formal proofs, leaving the user to suggest high-level strategies (referred to as tactics) for the proof assistant to try. Partial automation of the creation of the proof is often used to remove the largely mechanic action of proving simple subgoals. For example, the user might ask the proof engine to attempt to prove a statement by induction on a particular variable in an equation. The validity of each additional statement to the proof is confirmed, so that the final proof is known to be correct (assuming that the axioms are consistent, of course). Proof assistants are frequently reffered to as ``tactic provers'', or just ``provers''.
These grew out of of the desire to produce large and complex proofs without the pain of producing the proof manually. Robin Milner's Edinburgh LCF [37] incorporated a meta-language [38,44] (a formal symbolic language used to describe and reason about another language) enabling programmers to represent proof tactics for generalised logics. This idea of a meta-language (ML) spread to other proof assistants, including Paulson and Nipkow's Isabelle [43,41], Bates and Constable's Nuprl [17,52], and Gordon and Melham's HOL [22].
Other examples of proof assistants include Pollack's LEGO [33], Raffalli, Curmin, Manoury and Rozier's PhoX [48] and Paulin-Mohring et al's Coq [10].
|
|
|