CLI Reference
typedlogic
Usage:
typedlogic [OPTIONS] COMMAND [ARGS]...
Options:
--install-completion Install completion for the current shell.
--show-completion Show completion for the current shell, to copy it or
customize the installation.
--help Show this message and exit.
convert
Convert from one logic form to another.
For a list of supported parsers and compilers, see https://py-typedlogic.github.io/py-typedlogic/
Note that some conversions may be lossy. Currently no warnings are issued for such cases.
Example:
typedlogic convert my_theory.py -t fol
Usage:
typedlogic convert [OPTIONS] THEORY_FILES...
Options:
THEORY_FILES... [required]
-f, --input-format TEXT Input format; inferred from file suffix if
omitted
-t, --output-format TEXT Output format
-o, --output-file PATH Output file path
--validate-types / --no-validate-types
Use mypy to validate types [default:
validate-types]
--help Show this message and exit.
dump
Parse and combine multiple input files, then export to specified format without solving.
This command is useful for preprocessing, format conversion, and inspecting the combined logical theory before solving.
Files can be Python (.py) or YAML (.yaml) format - format is auto-detected.
Examples
# Combine and export to first-order logic
typedlogic dump theory.py facts.yaml -t fol -o combined.fol
# Export to YAML format
typedlogic dump axioms.py data.yaml -t yaml
# Combine multiple files and view as Prolog
typedlogic dump theory1.py theory2.py facts.yaml -t prolog
Usage:
typedlogic dump [OPTIONS] INPUT_FILES...
Options:
INPUT_FILES... [required]
-f, --input-format TEXT Input format; inferred from file suffix if
omitted
-t, --output-format TEXT Output format (fol, yaml, prolog, etc.)
[default: yaml]
-o, --output-file PATH Output file path
--validate-types / --no-validate-types
Use mypy to validate types [default:
validate-types]
--help Show this message and exit.
list-compilers
Lists all compilers.
Anything here should be usable as an output format.
Usage:
typedlogic list-compilers [OPTIONS]
Options:
--help Show this message and exit.
list-parsers
Lists all parsers.
Anything here should be usable as an input format.
Usage:
typedlogic list-parsers [OPTIONS]
Options:
--help Show this message and exit.
list-solvers
Lists all solvers.
Anything here should be usable as a solver.
Usage:
typedlogic list-solvers [OPTIONS]
Options:
--help Show this message and exit.
prove
Prove goal and lemma obligations embedded in a theory.
Goals and lemmas are not asserted as axioms. This command loads the base theory and asks the selected solver to prove each quoted obligation.
Usage:
typedlogic prove [OPTIONS] THEORY_FILE [DATA_FILES]...
Options:
THEORY_FILE [required]
-s, --solver TEXT Solver to use (z3, prover9, clingo, etc.)
[default: z3]
--target [all|goals|lemmas] Proof obligations to run: all, goals, or
lemmas. [default: all]
--validate-types / --no-validate-types
Use mypy to validate types [default:
validate-types]
-f, --input-format TEXT Input format; inferred from file suffix if
omitted
-d, --data-input-format TEXT Format for ground terms
--name TEXT Only prove obligations from a named goal or
lemma group. Repeat for multiple names.
--dump-program, --show-program Print the solver-specific generated program
before solving.
[DATA_FILES]...
--help Show this message and exit.
solve
Solve logical theories with facts using the specified solver.
Accepts a theory file and optional data files containing facts. Files can be Python (.py) or YAML (.yaml) format - format is auto-detected.
First checks satisfiability, then enumerates all models if satisfiable.
Examples
# Solve with theory and facts
typedlogic solve theory.py facts.yaml --solver z3
# Check satisfiability only
typedlogic solve theory.py --check-only
# Solve with multiple data files
typedlogic solve theory.py data1.yaml data2.yaml --solver z3
Usage:
typedlogic solve [OPTIONS] THEORY_FILE [DATA_FILES]...
Options:
THEORY_FILE [required]
-s, --solver TEXT Solver to use (z3, souffle, clingo, etc.)
[default: souffle]
-c, --check-only Check satisfiability only, do not enumerate
models
--validate-types / --no-validate-types
Use mypy to validate types [default:
validate-types]
-f, --input-format TEXT Input format; inferred from file suffix if
omitted
-d, --data-input-format TEXT Format for ground terms
-t, --output-format TEXT Output format
-o, --output-file PATH Output file path
--show, --predicate TEXT Only show materialized ground terms for
these predicates. Repeat for multiple
predicates.
--max-models INTEGER Stop after showing this many models
--dump-program, --show-program Print the solver-specific generated program
before solving.
[DATA_FILES]...
--help Show this message and exit.
test
Run quoted test_case(...) declarations and prove goals and lemmas embedded in a theory.
Tests are off by default for solve. This command opts into test metadata:
each given(that(...)) is temporarily asserted, and each expect(that(...))
is checked against the resulting solver state. Goal and lemma metadata is
also proved against the base theory unless --no-proofs is used.
Usage:
typedlogic test [OPTIONS] THEORY_FILE [DATA_FILES]...
Options:
THEORY_FILE [required]
-s, --solver TEXT Solver to use (z3, souffle, clingo, etc.)
[default: souffle]
--target [all|goals|lemmas] Proof obligations to run after test cases:
all, goals, or lemmas. [default: all]
--validate-types / --no-validate-types
Use mypy to validate types [default:
validate-types]
-f, --input-format TEXT Input format; inferred from file suffix if
omitted
-d, --data-input-format TEXT Format for ground terms
--test TEXT Only run a named test case. Repeat for
multiple tests.
--name TEXT Only prove obligations from a named goal or
lemma group. Repeat for multiple names.
--proofs / --no-proofs Also prove goal and lemma obligations.
[default: proofs]
--dump-program, --show-program Print the solver-specific generated program
before solving.
[DATA_FILES]...
--help Show this message and exit.