Predicate Logic

A Simple Propositional Example

The proof consists of two main branches, corresponding to the two directions of the equivalence. The first branch has all the subcells open, while the second one has all the subcells closed (in HTML they are represented by nested links).

Prove

with no assumptions.

Example With Quantifiers

Universally quantified formulae are used here in order to define the relation of congruence by bidirectional less-or-equal. Then, one proves that the this congruence is transitive by using the transitivity of the ordering relation.

Prove

under the assumption(s)

,

.

Example from Analysis

This is a more involved example in which we prove that the sum of two positive functions has limit 0 if each of them has limit 0. This is the only proof which was not produced completely automatically, but the prover was directed (in active mode) by the user. Namely, some assumptions were removed during the proof in order to minimize the search space, also the main existential conclusion was proved by proving first the right instance of it (with N = ]),
which was supplied interactively by the user.

Prove

under the assumption(s)

,

,

,

,

,

,

.