Skip to content

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. Currently supported: python,
                                  yaml, owlpy  [default: python]
  -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]
  -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.

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. Currently supported: python,
                                  yaml, owlpy  [default: python]
  -d, --data-input-format TEXT    Format for ground terms
  -t, --output-format TEXT        Output format
  -o, --output-file PATH          Output file path
  [DATA_FILES]...
  --help                          Show this message and exit.