nltk.inference.tableau module

Module for a tableau-based First Order theorem prover.

class nltk.inference.tableau.Agenda[source]

Bases: object

__init__()[source]
clone()[source]
mark_alls_fresh()[source]
mark_neqs_fresh()[source]
pop_first()[source]

Pop the first expression that appears in the agenda

put(expression, context=None)[source]
put_all(expressions)[source]
put_atoms(atoms)[source]
replace_all(old, new)[source]
class nltk.inference.tableau.Categories[source]

Bases: object

ALL = 20
AND = 10
APP = 4
ATOM = 0
D_NEG = 7
EQ = 18
EXISTS = 19
IFF = 16
IMP = 14
N_ALL = 8
N_AND = 15
N_APP = 5
N_ATOM = 2
N_EQ = 6
N_EXISTS = 9
N_IFF = 17
N_IMP = 12
N_OR = 11
N_PROP = 3
OR = 13
PROP = 1
class nltk.inference.tableau.Debug[source]

Bases: object

__init__(verbose, indent=0, lines=None)[source]
line(data, indent=0)[source]
exception nltk.inference.tableau.ProverParseError[source]

Bases: Exception

class nltk.inference.tableau.TableauProver[source]

Bases: Prover

static is_atom(e)[source]
class nltk.inference.tableau.TableauProverCommand[source]

Bases: BaseProverCommand

__init__(goal=None, assumptions=None, prover=None)[source]
Parameters

  • goal (sem.Expression) – Input expression to prove

  • assumptions (list(sem.Expression)) – Input expressions to use as assumptions in the proof.

nltk.inference.tableau.demo()[source]
nltk.inference.tableau.tableau_test(c, ps=None, verbose=False)[source]
nltk.inference.tableau.testHigherOrderTableauProver()[source]
nltk.inference.tableau.testTableauProver()[source]