Contents Menu Expand Light mode Dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content
unicode-fol-kit 0.13.1
unicode-fol-kit 0.13.1

Guide

  • Installation
  • Quickstart
  • Choosing a tool
  • Parsing and the AST
  • Transforming & exporting formulas
  • Classical FOL / MSFOL reasoning
  • Modal, temporal, epistemic & deontic logic
  • Quantified Modal Logic
  • Higher-order proving: Isabelle / THF exporters
  • Many-valued logic
  • Fuzzy (Łukasiewicz / BL) logic
  • Intuitionistic logic
  • Second-order logic
  • Description logic ALC
  • Hybrid logic H(@) — naming worlds
  • Relevant logic
  • Dependence logic and IF logic (team semantics)
  • Substructural logics: linear and Lambek
  • Further Non-Classical Logics
  • Natural-language translation targets
  • Syntax reference

Reference

  • API reference
    • unicode_fol_kit.MSFLParser
    • unicode_fol_kit.Node
    • unicode_fol_kit.substitute
    • unicode_fol_kit.free_variables
    • unicode_fol_kit.to_fol
    • unicode_fol_kit.to_nnf
    • unicode_fol_kit.to_pnf
    • unicode_fol_kit.to_cnf
    • unicode_fol_kit.to_dnf
    • unicode_fol_kit.to_tseitin_cnf
    • unicode_fol_kit.skolemize
    • unicode_fol_kit.is_horn
    • unicode_fol_kit.eliminate_lambdas
    • unicode_fol_kit.beta_eta_normalize
    • unicode_fol_kit.reduce_trace
    • unicode_fol_kit.unify
    • unicode_fol_kit.apply_subst
    • unicode_fol_kit.parse_tptp
    • unicode_fol_kit.parse_tptp_formula
    • unicode_fol_kit.load_tptp
    • unicode_fol_kit.parse_prover9
    • unicode_fol_kit.parse_prover9_problem
    • unicode_fol_kit.load_prover9
    • unicode_fol_kit.from_z3
    • unicode_fol_kit.parse_smtlib
    • unicode_fol_kit.load_smtlib
    • unicode_fol_kit.sanitize_names
    • unicode_fol_kit.sanitize_all
    • unicode_fol_kit.parse_latex
    • unicode_fol_kit.latex_to_unicode
    • unicode_fol_kit.to_english
    • unicode_fol_kit.prove
    • unicode_fol_kit.is_valid_resolution
    • unicode_fol_kit.is_valid
    • unicode_fol_kit.is_satisfiable
    • unicode_fol_kit.get_model
    • unicode_fol_kit.is_satisfiable_arith
    • unicode_fol_kit.is_valid_arith
    • unicode_fol_kit.formulas_are_equivalent
    • unicode_fol_kit.check_logical_entailment
    • unicode_fol_kit.check_logical_entailment_vampire
    • unicode_fol_kit.find_model
    • unicode_fol_kit.find_countermodel
    • unicode_fol_kit.is_satisfiable_finite
    • unicode_fol_kit.is_valid_finite
    • unicode_fol_kit.check_proof
    • unicode_fol_kit.find_fitch_proof
    • unicode_fol_kit.is_valid_fitch
    • unicode_fol_kit.render_fitch
    • unicode_fol_kit.check_sequent_proof
    • unicode_fol_kit.check_lj_proof
    • unicode_fol_kit.is_valid_tableau
    • unicode_fol_kit.prove_tableau
    • unicode_fol_kit.tableau_model
    • unicode_fol_kit.ill_prove
    • unicode_fol_kit.ill_derivable
    • unicode_fol_kit.check_ill_proof
    • unicode_fol_kit.lambek_prove
    • unicode_fol_kit.lambek_derivable
    • unicode_fol_kit.check_lambek_proof
    • unicode_fol_kit.satisfies_modal
    • unicode_fol_kit.standard_translation
    • unicode_fol_kit.is_modal_valid
    • unicode_fol_kit.modal_decide
    • unicode_fol_kit.modal_countermodel
    • unicode_fol_kit.modal_prove
    • unicode_fol_kit.qml_is_valid
    • unicode_fol_kit.qml_equivalent
    • unicode_fol_kit.hybrid_is_valid
    • unicode_fol_kit.to_thf_modal
    • unicode_fol_kit.to_isabelle_modal
    • unicode_fol_kit.isabelle_decide_modal
    • unicode_fol_kit.isabelle_decide_fol
    • unicode_fol_kit.modal_faithfulness_theory
    • unicode_fol_kit.intuitionistic_faithfulness_theory
    • unicode_fol_kit.conditional_faithfulness_theory
    • unicode_fol_kit.relevant_faithfulness_theory
    • unicode_fol_kit.truth_table
    • unicode_fol_kit.kleene_value
    • unicode_fol_kit.matrix_is_valid
    • unicode_fol_kit.matrix_entails
    • unicode_fol_kit.fuzzy_evaluate
    • unicode_fol_kit.fuzzy_is_valid
    • unicode_fol_kit.get_tnorm
    • unicode_fol_kit.int_valid
    • unicode_fol_kit.int_countermodel
    • unicode_fol_kit.satisfies_so
    • unicode_fol_kit.so_is_valid_finite
    • unicode_fol_kit.so_find_countermodel
    • unicode_fol_kit.minimal_entails
    • unicode_fol_kit.free_holds
    • unicode_fol_kit.announce
    • unicode_fol_kit.would
    • unicode_fol_kit.rel_valid
    • unicode_fol_kit.rel_countermodel
    • unicode_fol_kit.rel_satisfies
    • unicode_fol_kit.team_satisfies
    • unicode_fol_kit.team_models
    • unicode_fol_kit.dl
      • unicode_fol_kit.dl.concepts
      • unicode_fol_kit.dl.tableau
    • unicode_fol_kit.semantics.matrix
    • unicode_fol_kit.semantics.tnorm
    • unicode_fol_kit.semantics.free_logic
    • unicode_fol_kit.semantics.conditional
    • unicode_fol_kit.semantics.dynamic_epistemic
    • unicode_fol_kit.semantics.nonmonotonic
    • unicode_fol_kit.atp.modal_tableau
    • unicode_fol_kit.hol.isabelle_runner
  • Changelog
Back to top

Python Module Index

u
 
u
- unicode_fol_kit
    unicode_fol_kit.atp.modal_tableau
    unicode_fol_kit.dl
    unicode_fol_kit.dl.concepts
    unicode_fol_kit.dl.tableau
    unicode_fol_kit.hol.isabelle_runner
    unicode_fol_kit.semantics.conditional
    unicode_fol_kit.semantics.dynamic_epistemic
    unicode_fol_kit.semantics.free_logic
    unicode_fol_kit.semantics.matrix
    unicode_fol_kit.semantics.nonmonotonic
    unicode_fol_kit.semantics.tnorm
Copyright © 2026, Felix Vossel
Made with Sphinx and @pradyunsg's Furo