nltk.inference.tableau module

Module for a tableau-based First Order theorem prover.

exception nltk.inference.tableau.ProverParseError[source]

Bases: Exception

class nltk.inference.tableau.TableauProver[source]

Bases: nltk.inference.api.Prover

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

Bases: nltk.inference.api.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.

class nltk.inference.tableau.Agenda[source]

Bases: object

__init__()[source]
clone()[source]
put(expression, context=None)[source]
put_all(expressions)[source]
put_atoms(atoms)[source]
pop_first()[source]

Pop the first expression that appears in the agenda

replace_all(old, new)[source]
mark_alls_fresh()[source]
mark_neqs_fresh()[source]
class nltk.inference.tableau.Debug[source]

Bases: object

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

Bases: object

ATOM = 0
PROP = 1
N_ATOM = 2
N_PROP = 3
APP = 4
N_APP = 5
N_EQ = 6
D_NEG = 7
N_ALL = 8
N_EXISTS = 9
AND = 10
N_OR = 11
N_IMP = 12
OR = 13
IMP = 14
N_AND = 15
IFF = 16
N_IFF = 17
EQ = 18
EXISTS = 19
ALL = 20
nltk.inference.tableau.testTableauProver()[source]
nltk.inference.tableau.testHigherOrderTableauProver()[source]
nltk.inference.tableau.tableau_test(c, ps=None, verbose=False)[source]
nltk.inference.tableau.demo()[source]