nltk.inference.api

module documentation

(source)

Interfaces and base classes for theorem provers and model builders.

Prover is a standard interface for a theorem prover which tries to prove a goal from a list of assumptions.

ModelBuilder is a standard interface for a model builder. Given just a set of assumptions. the model builder tries to build a model for the assumptions. Given a set of assumptions and a goal G, the model builder tries to find a counter-model, in the sense of a model that will satisfy the assumptions plus the negation of G.

Class	`BaseModelBuilderCommand`	This class holds a `ModelBuilder`, a goal, and a list of assumptions. When build_model() is called, the `ModelBuilder` is executed with the goal and assumptions.
Class	`BaseProverCommand`	This class holds a `Prover`, a goal, and a list of assumptions. When prove() is called, the `Prover` is executed with the goal and assumptions.
Class	`BaseTheoremToolCommand`	This class holds a goal and a list of assumptions to be used in proving or model building.
Class	`ModelBuilder`	Interface for trying to build a model of set of formulas. Open formulas are assumed to be universally quantified. Both the goal and the assumptions are constrained to be formulas of `logic.Expression`.
Class	`ModelBuilderCommand`	This class holds a `ModelBuilder`, a goal, and a list of assumptions. When build_model() is called, the `ModelBuilder` is executed with the goal and assumptions.
Class	`ModelBuilderCommandDecorator`	A base decorator for the `ModelBuilderCommand` class from which other prover command decorators can extend.
Class	`ParallelProverBuilder`	This class stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.
Class	`ParallelProverBuilderCommand`	This command stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.
Class	`Prover`	Interface for trying to prove a goal from assumptions. Both the goal and the assumptions are constrained to be formulas of `logic.Expression`.
Class	`ProverCommand`	This class holds a `Prover`, a goal, and a list of assumptions. When prove() is called, the `Prover` is executed with the goal and assumptions.
Class	`ProverCommandDecorator`	A base decorator for the `ProverCommand` class from which other prover command decorators can extend.
Class	`TheoremToolCommand`	This class holds a goal and a list of assumptions to be used in proving or model building.
Class	`TheoremToolCommandDecorator`	A base decorator for the `ProverCommandDecorator` and `ModelBuilderCommandDecorator` classes from which decorators can extend.
Class	`TheoremToolThread`	Undocumented