Interactive tutorial

First-order logic with iProver

Learn the essentials of TPTP syntax, experiment with small problems, and follow a proof from submission to graph.

Introduction

This tutorial assumes a basic familiarity with first-order logic. It introduces the TPTP notation used to write first-order form (FOF) problems and lets you run each example directly in iProver.

Each editor below is live. Change the formula, check its syntax, then run iProver to see the result.

TPTP format

FOF problems are written as a series of statements. A theorem is usually expressed as axioms that are assumed to be true and a conjecture that should follow from them:

Ax₁ ∧ … ∧ Axₙ ⊨ Conjecture

A TPTP statement has the following general form:

language(name, role, formula, source, useful_info).

For the problems in this tutorial, the language is fof:

fof(name, role, formula, source, useful_info).

The name can contain letters, numbers, and underscores. We mainly use the axiom and conjecture roles. The role plain is commonly assigned to statements derived by iProver. The optional source and useful_info fields can be omitted here.

This is a trivially true conjecture:

fof(name, conjecture, (p(a) => p(a))).

Try removing a bracket or the final full stop, changing the case of a name, or adding a line break. Select Check syntax to see how strict the TPTP grammar is.

Live SSE Messages:

FOF syntax

The previous example uses the formula (p(a) => p(a)). Quantified formulas generally follow this shape:

<quantifier> [<variable_list>] : <formula>

Use ! for “for all” and ? for “there exists.” Multiple variables can share a quantifier. For example,![X, Y, Z]: (...) is equivalent to nesting three universal quantifiers. Variable names must begin with a capital letter, as in X, X1, or Num1.

Operator reference

~not (¬)

&and (∧)

|or (∨)

=is equal to (=)

!=is not equal to (≠)

<=>if and only if (⇔)

=>implies (⇒)

<=is implied by (⇐)

<~>is not equivalent to (⇎)

The following conjecture is true without any additional context. Run it, then explain what it says semantically.

Live SSE Messages:

Constants, functions, and predicates

Constants, such as a, b, and c. iProver may also introduce Skolem constants and functions such as sK0 and sK1.
Functions and predicates describe objects and relationships. Their behaviour is constrained through axioms.

![X,Y,Z]: ((product(X,Y)=Z & (is_zero(X) | is_zero(Y))) => is_zero(Z)).

![X,Y]: (product(X,Y) = product(Y,X)).

Together, these axioms describe a commutative product and state that a product with a zero argument is zero.

The next problem is satisfiable, so its conjecture does not follow from the axioms. Which axiom is missing? Add it and run iProver again.

Live SSE Messages:

Show hint

A mother cannot be the father.

Proof walkthrough

In this final example, use the sign rules to prove that the square of a number is non-negative. After the run completes, explore the proof graph and its highlighting controls.

Submission targetNot submitted yet

Active clauses

Clauses currently considered by iProver during the search.

No active clauses yet.

Live iProver output

SSE messages, proof output, options, and prover statistics.