Tactic-style Theorem Provers

Proofs in Nuprl are accomplished by repeatedly invoking tactics which refine goals to be proven into (usually simpler) subgoals. This kind of logic is called a Refinement Logic. [9][8] Here is a description of a few of Nuprl's basic tactics. These are sufficient for completing most elementary proofs. A hypothesis is either a type declaration for a variable or it is an assumption. The hypotheses and conclusion of a sequent are collectively referred to as clauses.

• D : Decompose the outermost connective in clause . This tactic provides access to the introduction and elimination rules in Nuprl's logic. This tactic accepts optional arguments for, for example, instantiation of quantifiers.
• Ind : Do induction on declaration . The declaration must involve some inductively defined datatype: for example or T List for some type T.

• Assert : Split proof into two parts: one to prove , the other assuming to prove the original goal. This invokes Nuprl's cut rule.
• Decide : Case split on whether proposition is true or false.

• Auto: Do various kinds of automatic reasoning, including checking if conclusion is same as some assumption, certain decompositions, type checking, solving equalities and solving inequalities involving linear arithmetic expressions.

• Backchain : Repeatedly back-chain using assumptions and lemmas . This tactic is Nuprl's version of a Prolog-style resolution inference procedure.

• ArithSimp : Put arithmetic expressions in clause into a normal form.

• RewriteWith Rewrite clause using assumptions and lemmas .

• THEN , ORELSE , Repeat : These are tacticals used for joining together tactics. THEN sequences tactics, ORELSE allows trying alternative tactics and Repeat repeatedly applies a tactic.