LP, the Larch Prover -- Inconsistency


An inconsistency is a formula that is logically false.

LP automatically recognizes the formula x ~= t, where t is a term not involving the variable x, as inconsistent. Thus, LP rules out empty sorts. It also recognizes the formulas false and b = t, where t is a term not involving the boolean variable b, as inconsistent. Thus, the boolean sort contains two distinct values.

If an inconsistency arises during a proof by contradiction, that proof succeeds. If it arises during a proof by cases, the current case is deemed impossible.