unicode-fol-kit

A Python toolkit for first-order logic with Unicode operators — parse, transform, and reason about formulas — with a reasoning layer that reaches well beyond classical FOL into modal, temporal, many-valued, fuzzy, intuitionistic, second-order, description, and a range of non-classical logics.

from unicode_fol_kit import MSFLParser, is_valid

phi = MSFLParser().parse("∀x (Human(x) → Mortal(x)) ∧ Human(socrates) → Mortal(socrates)")
print(is_valid(phi))   # True

One parser class (MSFLParser) feeds a full reasoning stack: four proof methods (a built-in resolution prover, Fitch natural deduction with checker and searcher, the Gentzen sequent calculi LK/LJ, and analytic tableaux), a finite model finder, SMT (Z3) and external-prover (Prover9/Vampire) backends, truth tables, and dedicated semantics for every logic. Formulas import/export to TPTP, Prover9, SMT-LIB, LaTeX, and JSON.

Where to start

• New here? Read Installation then Quickstart.

• Looking for a specific capability? The Choosing a tool page maps a question (and a logic) to the entry point that answers it.

• Want the exact signature of a function? See the API reference reference.

Guide

• Installation
  • Supported Python
  • Via pip
  • Via git clone
  • Verify the install
  • Optional external tools
• Quickstart
  • The one import you always start with
  • Parse and check validity
  • Satisfiability and reading out a model
  • Prove an entailment without any external solver
  • Find a finite first-order model
  • Finding counterexamples
  • Read a formula back as English
  • Round-trip to Unicode and LaTeX
  • Working with propositional operators and precedence
  • An end-to-end vignette
  • One non-classical taster: modal validity
  • Another taster: a three-valued truth table
  • Formula normalization and transformation
  • Extracting formula information
  • When parsing fails
  • Next steps
• Choosing a tool
  • Which tool for which question
  • Worked recipes
  • Logics supported
  • Composing parser modes
  • The frontier families
• Parsing and the AST
  • Parser modes
  • Unicode surface syntax
  • Natural-language constructs
  • Lambda syntax
  • ASCII tree view
  • Graphviz DOT view
  • Inspection API
  • Unicode round-trip
  • JSON round-trip
  • The error model: NamingError vs ParsingError
• Transforming & exporting formulas
  • Normal forms
  • Sort relativisation: to_fol()
  • Lambda-calculus operations
  • Traversal and inspection
  • Import
• Classical FOL / MSFOL reasoning
  • Built-in resolution prover
  • Satisfiability, validity, and models (Z3)
  • Equivalence checking (Z3)
  • External provers (Prover9 / Vampire)
  • Natural deduction (Fitch proofs)
  • Finding Fitch proofs (backtracking search)
  • Sequent calculus (Gentzen LK, incl. second-order)
  • Sequent calculus — intuitionistic LJ
  • Analytic tableaux
  • Finite model finder
  • Truth tables (propositional)
• Modal, temporal, epistemic & deontic logic
  • Parsing modal mode
  • Evaluating over a Kripke model
  • Standard translation to FOL
  • Deciding modal validity — the native tableau (0.9.0)
  • Future temporal operators over a flow of time
  • Past-tense temporal operators (0.9.0)
  • More frames: B, S4.2, S4.3, GL
  • End-to-end: parse, decide, refute, translate
• Quantified Modal Logic
  • Building modal formulas as nodes
  • Semantics: per-world domains and actualist quantifiers
  • (A) First-order shallow embedding → Z3
  • (B) Higher-order shallow embedding → TPTP THF
  • End-to-end: parse → decide → cross-check → export
• Higher-order proving: Isabelle / THF exporters
  • What the exporters emit (and what they cannot decide)
  • Classical FOL: to_thf_fol / to_isabelle_fol
  • Many-sorted FOL: to_thf_msfol / to_isabelle_msfol
  • Second-order: to_thf_so / to_isabelle_so
  • The full modal family: to_thf_modal_full / to_isabelle_modal
  • A sample emitted Isabelle theory
  • Intuitionistic logic: the GMT translation
  • Three-valued K3 / LP (bonus exporters)
  • Actually running it: the Isabelle runner
  • Deep and shallow embeddings with faithfulness proofs
• Many-valued logic
  • Three-valued evaluation: kleene_value
  • Truth tables: truth_table
  • Three-valued decisions: is_valid / is_satisfiable / entails
  • Finite matrices: semantics.matrix
  • Building a custom matrix
  • End-to-end: parse → decide → tabulate
• Fuzzy (Łukasiewicz / BL) logic
  • Parsing fuzzy formulas (FL / MSFL mode)
  • fuzzy_evaluate — truth degree under a valuation
  • The three t-norms
  • fuzzy_is_satisfiable / fuzzy_is_valid / fuzzy_get_model (Z3 reals)
  • Quantifier grounding (0.9.0)
  • Building fuzzy nodes directly
  • End-to-end: a small fuzzy rule base
• Intuitionistic logic
  • Propositional validity and counter-models
  • First-order intuitionistic logic
  • LJ sequent-calculus proofs
  • Cross-check: the Gödel–McKinsey–Tarski embedding into S4
• Second-order logic
  • Parsing: ∀P / ∃P with inferred arity
  • Finite-model evaluation: satisfies_so / holds
  • Bounded second-order search (new in 0.9.0)
  • Building SO nodes directly
  • Exporting to a HOL prover
  • Scope
• Description logic ALC
  • Concept constructors
  • Rendering
  • Negation normal form
  • Reasoning API
  • General TBoxes
  • ABoxes
  • Cyclic TBoxes terminate
  • End-to-end: a small family ontology
• Hybrid logic H(@) — naming worlds
  • Syntax
  • Evaluating with a nominal assignment
  • The standard translation: nominals as world constants
  • Deciding validity: hybrid_is_valid
  • The honest boundary
• Relevant logic
  • Why relevance?
  • The simplified Routley–Meyer semantics
  • Validity and the headline failures
  • Reading a countermodel
  • Building a model by hand
  • The bounded-validity contract
  • Beyond B: why the toolkit ships B
• Dependence logic and IF logic (team semantics)
  • Teams as information states
  • Dependence atoms are functional dependencies
  • The splitting disjunction
  • Quantifiers, sentences, and the |dom| = 1 example
  • Slashed quantifiers and imperfect information
  • A genuine dependence sentence: the universal sink
  • The honest boundary
• Substructural logics: linear and Lambek
  • Resources, not truths — why A ⊬ A ⊗ A
  • The connective tour, vending-machine style
  • ! as banking
  • The Lambek calculus as grammar
  • Decidability status — what a None means
  • The honest boundary: no classical export
• Further Non-Classical Logics
  • Free logic
  • Public announcement / dynamic epistemic logic
  • Counterfactual conditionals
  • Circumscription / non-monotonic entailment
  • Further non-classical families
• Natural-language translation targets
  • Counting quantifier — Count (∃≥n / ∃≤n / ∃=n)
  • Degree term — Measure (μ)
  • Cardinality term — Cardinality (|{v : φ}|)
  • Concessive connective — Contrast (Ⓒ)
  • Attitude operators — Says / Wants
  • Reading Prover9 files
  • Making imported names re-parseable — sanitize_names
  • Cross-mode availability
• Syntax reference
  • Tokens
  • Terms
  • Atomic formulas
  • Compound formulas
  • Operator precedence
  • Mixing same-level operators
  • Quantifier scope
  • Supported symbols
  • Lambda abstraction and application (all modes)
  • A complete example per mode
  • AST nodes
  • Error handling

Reference

• API reference
• Changelog

Indices

• Index

• Module Index

• Search Page