API reference

Auto-generated from the package docstrings. The tables below link to the full signature and documentation of each public entry point; use the search box or the Index for anything not listed here.

Parsing & the AST

MSFLParser	Unified parser supporting FOL, MSFOL, MSFL, FL, modal, and second-order modes.
Node	Base class for all AST nodes.
substitute	Substitute target with replacement in term, with full capture avoidance.
free_variables	Return the set of free Variable and LambdaVar occurrences in node.
to_fol	Reduce an MSFL (or plain FOL) node to a purely classical FOL node.

Normal forms, lambda calculus & unification

to_nnf	Return the negation normal form of node (after reducing to classical FOL).
to_pnf	Return the prenex normal form: quantifier prefix over a quantifier-free NNF matrix, with all bound variables standardised apart.
to_cnf	Return prenex form whose matrix is a conjunction of clauses.
to_dnf	Return prenex form whose matrix is a disjunction of conjunctive clauses.
to_tseitin_cnf	Return an EQUISATISFIABLE CNF via the Tseitin/definitional encoding.
skolemize	Return prenex NNF with existentials replaced by Skolem terms.
is_horn	Return True iff node's clausal form consists of Horn clauses.
eliminate_lambdas	Return a lambda-free node ready for the FOL export / normal-form pipeline.
beta_eta_normalize	Reduce node to beta-eta normal form by alternating beta_reduce and eta_reduce.
reduce_trace	Return the leftmost-outermost reduction trace from node to beta-normal form.
unify	Most-general unifier of t1 and t2, or None if they do not unify.
apply_subst	Apply substitution subst to node, returning a new node.

Import / export

parse_tptp	Parse a whole TPTP problem into a list of TptpFormula records.
parse_tptp_formula	Parse a single bare TPTP FOF/CNF formula (no fof(...) wrapper) into a Node.
load_tptp	Read a TPTP problem file and parse_tptp() its contents.
parse_prover9	Parse a single Prover9-syntax formula into a toolkit Node.
parse_prover9_problem	Parse a whole Prover9 / LADR input file into a list of Prover9Formula.
load_prover9	Read a Prover9 / LADR input file and parse_prover9_problem() its contents.
from_z3	Convert a Z3 expression (z3.ExprRef) into a toolkit Node.
parse_smtlib	Parse an SMT-LIB2 string and return its assertions as toolkit Nodes.
load_smtlib	Read an SMT-LIB2 (.smt2) file and parse_smtlib() its contents.
sanitize_names	Return (sanitized_node, mapping) with all names rewritten to legal tokens.
sanitize_all	Sanitize a sequence of formulas with one shared, consistent NameMapping.
parse_latex	Parse a LaTeX math-mode formula into an AST node.
latex_to_unicode	Translate a LaTeX math-mode formula into the toolkit's Unicode surface syntax.
to_english	Return an English paraphrase of node (best-effort, not a parse inverse).

Classical reasoning

prove	Return True iff premises entail conclusion (premises ⊨ conclusion).
is_valid_resolution	Return True iff formula is valid (its negation is refutable).
is_valid	Return True if the formula is valid, i.e. its negation is unsatisfiable.
is_satisfiable	Return True if the formula has a model (Z3 reports sat).
get_model	Return a satisfying assignment as a dict, or None if unsat/unknown.
is_satisfiable_arith	Return True iff formula has a model under interpreted arithmetic.
is_valid_arith	Return True iff formula is valid under interpreted arithmetic.
formulas_are_equivalent	Return True iff formula1 and formula2 are logically equivalent.
check_logical_entailment	Checks if a conclusion entails from the defined premises by using prover9.
check_logical_entailment_vampire	Return whether premises entail conclusion, decided by Vampire.
find_model	Return a finite Structure satisfying every formula, or None.
find_countermodel	Return a finite structure satisfying premises but not conclusion, or None.
is_satisfiable_finite	True iff formula has a finite model of size ≤ max_size (bounded).
is_valid_finite	True iff no finite countermodel of formula exists up to max_size (bounded).

Proof systems

check_proof	Return True iff proof is a valid Fitch derivation (sound).
find_fitch_proof	Search for a Fitch proof of premises ⊢ conclusion; return it or None.
is_valid_fitch	Return True iff formula is provable from no premises (a found-theorem check).
render_fitch	Render proof in classic Fitch notation as a multi-line string.
check_sequent_proof	Return True iff derivation is a valid sequent-calculus derivation (sound).
check_lj_proof	Return True iff derivation is a valid intuitionistic LJ derivation (sound).
is_valid_tableau	Return True iff formula is valid — its negation's tableau closes.
prove_tableau	Return True iff premises entail conclusion (premises + ¬conclusion close).
tableau_model	Return a satisfying literal assignment if formulas are satisfiable, else None.
ill_prove	Search for a cut-free ILL derivation of antecedents ⊢ goal.
ill_derivable	Return True iff ill_prove() finds a derivation of antecedents ⊢ goal.
check_ill_proof	Return True iff derivation is a valid cut-free ILL derivation (sound).
lambek_prove	Decide sequence ⊢ goal in the Lambek calculus L; return a derivation or None.
lambek_derivable	Return True iff sequence ⊢ goal is derivable in L (a decision procedure).
check_lambek_proof	Return True iff derivation is a valid cut-free L derivation (sound).

Modal, temporal, epistemic & deontic logic

satisfies_modal	Return whether formula is true at world in the Kripke model.
standard_translation	Translate a propositional modal formula into a classical FOL Node.
is_modal_valid	Return True iff formula is modally valid over frame — ¬formula closes.
modal_decide	Decide formula over frame: "valid" / "invalid" / "unknown".
modal_countermodel	Return a Kripke model falsifying formula over frame, or None.
modal_prove	Return True iff premises locally entail conclusion over frame.
qml_is_valid	Return True iff formula is QML-valid under mode / frame (via Z3).
qml_equivalent	Return True iff two modal formulas are QML-equivalent under mode / frame.
hybrid_is_valid	Return True iff the hybrid-modal formula is valid over frame (via Z3).
to_thf_modal	Emit a Benzmüller-style TPTP THF shallow embedding of formula.
to_isabelle_modal	Emit a complete, loadable Isabelle/HOL theory shallow-embedding formula.
isabelle_decide_modal	Decide a modal formula's validity by running a local Isabelle.
isabelle_decide_fol	Decide a classical FOL (or MSFOL) formula's validity by running Isabelle.
modal_faithfulness_theory	Emit the self-contained modal deep/maximal/minimal + faithfulness theory.
intuitionistic_faithfulness_theory	Emit the self-contained intuitionistic deep/maximal/minimal + faithfulness theory.
conditional_faithfulness_theory	Emit the self-contained Lewis-conditional deep/maximal/minimal + faithfulness theory.
relevant_faithfulness_theory	Emit the self-contained relevant-B deep/maximal/minimal + faithfulness theory.

Many-valued, fuzzy, intuitionistic & second-order

truth_table	Compute the TruthTable of a propositional formula under logic.
kleene_value	Strong-Kleene three-valued truth value of a classical formula.
matrix_is_valid	True iff formula is designated under every assignment over matrix.
matrix_entails	True iff every assignment designating all premises designates conclusion.
fuzzy_evaluate	Compute the fuzzy truth degree in [0, 1] of an FL/MSFL formula.
fuzzy_is_valid	Return True iff the formula has degree 1 under every atom-valuation.
get_tnorm	Return the TNorm for name ("lukasiewicz" / "godel" / "product").
int_valid	Return True iff no intuitionistic counter-model to formula is found.
int_countermodel	Return (model, world) where formula fails intuitionistically, or None.
satisfies_so	Return whether structure satisfies formula (second-order Tarski).
so_is_valid_finite	True iff no finite counter-model of the SO formula is found up to max_size.
so_find_countermodel	Return a finite structure in which the SO formula FAILS, or None (bounded).
minimal_entails	Return whether premises circumscriptively entail conclusion (bounded).
free_holds	Convenience: free_satisfies of a closed formula (empty assignment).
announce	Return model updated by a truthful public announcement of formula.
would	Return whether world ⊨ antecedent □→ consequent (Lewis "would" counterfactual).
rel_valid	Return True iff no B-countermodel to formula is found within the bound.
rel_countermodel	Return (model, world) where formula fails at a normal world, or None.
rel_satisfies	Return whether formula is true at world in model.
team_satisfies	Return whether team satisfies formula in structure.
team_models	Return whether the structure makes the SENTENCE true: {∅} ⊨ formula.

Subpackage modules

dl	The dl subpackage — the description logic ALC.
semantics.matrix	Finite-valued logical matrices: a generalisation of the K3 / LP three-valued layer.
semantics.tnorm	Continuous t-norms for the fuzzy (BL / Hájek basic-logic) family.
semantics.free_logic	Free logic — first-order logic without the existence assumption.
semantics.conditional	Counterfactual conditionals — Lewis / Stalnaker sphere semantics.
semantics.dynamic_epistemic	Public announcement logic (PAL) — dynamic epistemic model update.
semantics.nonmonotonic	Non-monotonic reasoning — minimal-model entailment (predicate circumscription).
atp.modal_tableau	Labelled analytic tableaux for the propositional modal family.
hol.isabelle_runner	Run a local Isabelle to actually discharge the emitted shallow-embedding theories — turning the unicode_fol_kit.hol exporters from emit into proven / refuted.