TypedLogic CLI Tutorial
This tutorial demonstrates how to use the TypedLogic command-line interface (CLI) to work with logical theories and facts. The CLI provides powerful tools for:
- Converting between different logical formats
- Solving logical theories with various solvers
- Dumping combined theories for inspection and preprocessing
We'll explore these capabilities using practical examples with the familiar path-finding domain from previous tutorials.
CLI Overview
Let's start by exploring the available CLI commands:
%%bash
# Show CLI help
typedlogic --help
The CLI provides three main commands:
convert- Transform between different logical formatssolve- Solve logical theories with various solversdump- Combine and export theories without solving
Let's explore each in detail.
Setting Up Example Files
First, let's create some example files to work with. We'll use a simple path-finding theory similar to previous tutorials:
%%bash
# Create a directory for our examples
mkdir -p /tmp/typedlogic_cli_tutorial
mkdir -p /tmp/typedlogic_cli_tutorial/usa
mkdir -p /tmp/typedlogic_cli_tutorial/europe
cd /tmp/typedlogic_cli_tutorial
%%writefile /tmp/typedlogic_cli_tutorial/paths_theory.py
"""Path-finding logical theory with transitivity."""
from pydantic import BaseModel
from typedlogic import FactMixin
from typedlogic.decorators import axiom
ID = str
class Link(BaseModel, FactMixin):
"""A direct connection between two locations."""
source: ID
target: ID
class Path(BaseModel, FactMixin):
"""A path (possibly multi-hop) between two locations."""
source: ID
target: ID
@axiom
def link_implies_path(x: ID, y: ID):
"""Every direct link implies a path."""
assert Link(source=x, target=y) >> Path(source=x, target=y)
@axiom
def transitivity(x: ID, y: ID, z: ID):
"""Paths are transitive: if x->y and y->z, then x->z."""
assert (Path(source=x, target=y) & Path(source=y, target=z)) >> Path(source=x, target=z)
%%writefile /tmp/typedlogic_cli_tutorial/usa/Link.csv
source,target
CA,NV
NV,AZ
AZ,UT
CA,OR
OR,WA
WA,ID
ID,MT
%%writefile /tmp/typedlogic_cli_tutorial/europe/Link.csv
source,target
FR,DE
DE,PL
FR,IT
IT,CH
CH,DE
1. The convert Command
The convert command transforms logical theories from one format to another. This is useful for:
- Viewing theories in different representations
- Preparing input for external tools
- Understanding the formal semantics of your theories
%%bash
# Show convert command help
typedlogic convert --help
Convert to First-Order Logic (FOL)
Let's convert our Python theory to first-order logic:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic convert paths_theory.py -t fol
Convert to Prolog
Now let's see the same theory in Prolog format:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic convert paths_theory.py -t prolog
Convert to YAML
YAML format is useful for inspection and interchange:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic convert paths_theory.py -t yaml
Save Output to File
You can save the converted output to a file:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic convert paths_theory.py -t fol -o paths_theory.fol
echo "=== Contents of paths_theory.fol ==="
cat paths_theory.fol
2. The dump Command
The dump command combines multiple input files and exports them in a specified format without solving. This is useful for:
- Preprocessing and combining theories with facts
- Format conversion of combined datasets
- Inspecting the merged theory before solving
Parse and combine multiple input files, then export to specified format
without solving.
[2mThis command is useful for preprocessing, format conversion, and inspecting [0m
[2mthe combined logical theory before solving.[0m
[2mFiles can be Python (.py), YAML (.yaml), or CSV (.csv) format - format is auto-detected.[0m
[2mExamples [0m[1;2;36m--------[0m[2m ```bash # Combine and export to first-order logic typedlogic[0m
[2mdump theory.py facts.csv [0m[1;2;32m-t[0m[2m fol [0m[1;2;32m-o[0m[2m combined.fol[0m
[2m# Export to YAML format typedlogic dump axioms.py data.csv [0m[1;2;32m-t[0m[2m yaml[0m
[2m# Combine multiple files and view as Prolog typedlogic dump theory1.py [0m
[2mtheory2.py facts.csv [0m[1;2;32m-t[0m[2m prolog ```[0m
Combine Theory with Facts
Let's combine our theory with the USA links CSV data:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic dump paths_theory.py usa/Link.csv -t yaml
Combine Multiple Data Files
We can combine multiple CSV data files with the theory:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic dump paths_theory.py usa/Link.csv europe/Link.csv -t yaml
Export to Different Formats
The combined theory can be exported to various formats:
%%bash
cd /tmp/typedlogic_cli_tutorial
echo "=== Prolog Format ==="
typedlogic dump paths_theory.py usa/Link.csv -t prolog
echo -e "\n=== TPTP Format ==="
typedlogic dump paths_theory.py usa/Link.csv -t tptp
3. The solve Command
The solve command is the most powerful CLI feature. It combines logical theories with facts, checks satisfiability, and enumerates models. This supports:
- Multiple solver backends (Z3, Clingo, Souffle, etc.)
- Satisfiability checking before model enumeration
- Comprehensive error reporting and validation
Solve logical theories with facts using the specified solver.
[2mAccepts a theory file and optional data files containing facts. Files can be [0m
[2mPython (.py), YAML (.yaml), or CSV (.csv) format - format is auto-detected.[0m
[2mFirst checks satisfiability, then enumerates all models if satisfiable.[0m
[2mExamples [0m[1;2;36m--------[0m[2m ```bash # Solve with theory and facts typedlogic solve [0m
[2mtheory.py facts.csv [0m[1;2;36m-[0m[1;2;36m-solver[0m[2m z3[0m
[2m# Check satisfiability only typedlogic solve theory.py [0m[1;2;36m-[0m[1;2;36m-check[0m[1;2;36m-only[0m
[2m# Solve with multiple data files typedlogic solve theory.py data1.csv [0m
[2mdata2.csv [0m[1;2;36m-[0m[1;2;36m-solver[0m[2m z3 ```[0m
Basic Solving with clingo
Let's solve our path theory with the USA links using the clingo solver:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic solve paths_theory.py usa/Link.csv --solver clingo
Check Satisfiability Only
Sometimes you only want to check if a theory is satisfiable without enumerating models:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic solve paths_theory.py usa/Link.csv --solver z3 --check-only
Using Different Solvers
TypedLogic supports multiple solvers. Let's try the SnakeLog solver (pure Python datalog):
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic solve paths_theory.py usa/Link.csv --solver snakelog
Multiple Data Files
You can solve with multiple data files:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic solve paths_theory.py usa/Link.csv europe/Link.csv --solver snakelog
Save Results to File
You can save the solving results to a file:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic solve paths_theory.py usa/Link.csv europe/Link.csv --solver snakelog -o results.txt
echo "=== Contents of results.txt ==="
tail results.txt
4. Advanced Examples
Working with Contradictions
Let's create a theory with a contradiction to see how the CLI handles unsatisfiable theories:
%%writefile /tmp/typedlogic_cli_tutorial/contradictory_theory.py
"""A theory with contradictory axioms."""
from pydantic import BaseModel
from typedlogic import FactMixin
from typedlogic.decorators import axiom
ID = str
class Person(BaseModel, FactMixin):
name: ID
class Mortal(BaseModel, FactMixin):
name: ID
class Immortal(BaseModel, FactMixin):
name: ID
# Facts will be loaded from CSV as 'fact' predicate
class fact(BaseModel, FactMixin):
type: str
name: ID
@axiom
def person_from_fact(x: ID):
"""Extract Person facts from generic fact entries."""
assert fact(type="Person", name=x) >> Person(name=x)
@axiom
def immortal_from_fact(x: ID):
"""Extract Immortal facts from generic fact entries."""
assert fact(type="Immortal", name=x) >> Immortal(name=x)
@axiom
def all_persons_mortal(x: ID):
"""All persons are mortal."""
assert Person(name=x) >> Mortal(name=x)
@axiom
def contradiction(x: ID):
"""No one can be both mortal and immortal."""
assert ~(Mortal(name=x) & Immortal(name=x))
%%writefile /tmp/typedlogic_cli_tutorial/fact.csv
type,name
Person,Socrates
Immortal,Socrates
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic solve contradictory_theory.py fact.csv --solver z3
Type Validation
The CLI can validate Python files using mypy before processing:
%%bash
cd /tmp/typedlogic_cli_tutorial
# With type validation (default)
typedlogic solve paths_theory.py usa/Link.csv --solver z3 --check-only --validate-types
5. Practical Workflow Examples
Development Workflow
Here's a typical development workflow using the CLI:
%%bash
cd /tmp/typedlogic_cli_tutorial
echo "1. First, inspect the combined theory:"
typedlogic dump paths_theory.py usa_links.csv -t fol
echo -e "\n2. Check if theory + facts are satisfiable:"
typedlogic solve paths_theory.py usa_links.csv --solver z3 --check-only
echo -e "\n3. If satisfiable, solve and examine models:"
typedlogic solve paths_theory.py usa_links.csv --solver z3
Batch Processing
You can use the CLI in scripts for batch processing:
%%bash
cd /tmp/typedlogic_cli_tutorial
# Process multiple datasets
for dataset in usa_links.csv europe_links.csv; do
echo "=== Processing $dataset ==="
typedlogic solve paths_theory.py "$dataset" --solver z3 --check-only
done
Converting for External Tools
Convert theories to formats suitable for external tools:
%%bash
cd /tmp/typedlogic_cli_tutorial
# Export to TPTP for theorem provers
typedlogic dump paths_theory.py usa_links.csv -t tptp -o paths.tptp
# Export to Prolog for Prolog systems
typedlogic dump paths_theory.py usa_links.csv -t prolog -o paths.pl
echo "Generated files:"
ls -la *.tptp *.pl
6. Error Handling and Debugging
The CLI provides comprehensive error handling. Let's see some examples:
Invalid File Formats
The CLI gracefully handles invalid files:
%%bash
cd /tmp/typedlogic_cli_tutorial
echo "This is not valid CSV content: unclosed,quotes,\"here" > invalid.csv
typedlogic solve paths_theory.py invalid.csv --solver z3 --check-only || echo "Command failed as expected"
Unknown Solvers
Using an unknown solver produces a helpful error:
%%bash
cd /tmp/typedlogic_cli_tutorial
typedlogic solve paths_theory.py usa_links.csv --solver nonexistent_solver || echo "Command failed as expected"
7. Performance and Solver Comparison
Different solvers have different strengths. Let's compare their behavior:
%%bash
cd /tmp/typedlogic_cli_tutorial
echo "=== Z3 Solver ==="
time typedlogic solve paths_theory.py usa_links.csv --solver z3 --check-only
echo -e "\n=== SnakeLog Solver ==="
time typedlogic solve paths_theory.py usa_links.csv --solver snakelog --check-only
Summary
The TypedLogic CLI provides three powerful commands:
convert- Transform theories between formats (Python ↔ FOL, Prolog, YAML, etc.)dump- Combine multiple files and export without solving (great for preprocessing)solve- Full logical reasoning with satisfiability checking and model enumeration
Key Features:
- Multi-file support: Combine theories with multiple fact files
- Format auto-detection: Handles .py, .yaml, and .csv files automatically
- Multiple solvers: Z3, Clingo, Souffle, SnakeLog, and more
- Satisfiability checking: Always checks SAT before model enumeration
- Type validation: Optional mypy validation for Python files
- Comprehensive error handling: Clear error messages and validation
Common Workflows:
- Development:
dump→solve --check-only→solve - Debugging: Use
convertto inspect formal semantics - Integration: Use
dumpto export for external tools - Batch processing: Script multiple
solvecalls
The CLI makes TypedLogic accessible for both interactive exploration and automated processing pipelines.
Cleanup
Clean up our tutorial files:
%%bash
# Clean up tutorial files
rm -rf /tmp/typedlogic_cli_tutorial
echo "Tutorial cleanup complete!"