ProveProp

The ProveProp  family of tactics are useful for partially or completely proving goals that involve simple propositional reasoning. The strategy is basically to that for classical tableau  : Propositions in hypotheses and the conclusion are exhaustively decomposed and applications of the Hypothesis tactic are sought. A slight tweak is the tactic has to do `or' branching and backtracking when it tackles an conclusion or an or hypothesis, because the Nuprl sequents only allow one conclusion rather than many as is commonly the case in classical sequent calculi.

ProveProp

The basic tactic. Fails if doesn't succeed in solving all main goals.

ProveProp1

Like ProveProp, but leaves main subgoals at `or' branching points of the search for a solution when the search down every branch fails.

Like ProveProp1, but tries running tactic T before completely abandoning a search path. If T creates any main subgoals, search continues on these subgoals.

ProveProp is not complete for intuitionistic propositional logic  , because it always thins and hypotheses that are decomposed.