Using the Python API to create theories directly

In the previous tutorial we say how to write theories as Python programs. This allows for management of logical sentences as Python programs.

It is possible to bypass this step as use the Python data models directly, without any need for parsing from Python.

Creating a Theory object

The top-level holder for logical sentences is a Theory object. Minimally a theory object can hold a number of logical sentences, as well as predicate definitions.

We'll create a Theory object with minimal metadata:

from typedlogic import Theory

theory = Theory("my theory")

Adding type definitions

Next we will add some definitions of types. This step is optional, as you can simply use base types like str, int - or even leave your arguments untyped.

But adding custom types can help make the program more understandable, and can help catch common errors, as well as help work better with frameworks like Souffle that expect typing information.

theory.type_definitions = {
    "ID": "str",
    "PersonID": "ID",
    "PetID": "ID",
    "SpeciesEnum": "str",
    "Age": ["int", "float"]
}

Here we added some identifier types, as well as a type for stroing ages which is a union of int and float

Adding predicate definitions

Next we need to add PredicateDefinitions. These are the equivalent to the python classes we declared in the previous tutorial. Minimally, they describe the arguments (attributes, in Python speak) which predicates (classes) can take.

from typedlogic import PredicateDefinition


Person = PredicateDefinition("Person", {"name": "PersonID", "age": "Age"})
Pet = PredicateDefinition("Pet", {"name": "PetID", "owner": "PersonID", "species": "SpeciesEnum"})
theory.predicate_definitions = [Person, Pet]

Here we added predicate definitions for two predicates, Person/2, and Pet/3 (the / nomenclature is often used to denote the number of arguments).

Next we will show what happens when we compile this to an alternative representation (here, Souffle)

from typedlogic.registry import get_compiler, get_solver

compiler = get_compiler("souffle")
print(compiler.compile(theory))

.type Id = symbol
.type Personid = symbol
.type Petid = symbol
.type Speciesenum = symbol
.type Age = number | number
.decl Person(name: Personid, age: Age)
.decl Pet(name: Petid, owner: Personid, species: Speciesenum)

Adding logical sentences

Here we will define a new predicate CatOwner/1 and a rule-type axiom to infer membership.

CatOwner = PredicateDefinition("CatOwner", {"name": "PersonID"})
theory.predicate_definitions.append(CatOwner)

from typedlogic import Term, Variable, Forall
x = Variable("x")
y = Variable("y")
theory.add(
    Forall([x, y],
            Term("Pet", x, y, "CAT") >> Term("CatOwner", y)
           )
)

Here the >> is syntactic sugar for Implies.

The Term represents the "atomic" unit of sentences.

Let's see what this looks like in Souffle syntax:

print(compiler.compile(theory))

.type Id = symbol
.type Personid = symbol
.type Petid = symbol
.type Speciesenum = symbol
.type Age = number | number
.decl Person(name: Personid, age: Age)
.decl Pet(name: Petid, owner: Personid, species: Speciesenum)
.decl CatOwner(name: Personid)
CatOwner(y) :- Pet(x, y, "CAT").

Adding ground terms (facts)

Next we will add ground terms (or simply instances in Python speak). We will use Term objects again, but these are ground terms (no variables).

theory.add(Term("Person", "Freddy", 22))
theory.add(Term("Pet", "Mr Tickles", "Freddy", "CAT"))

Using a Solver

Next we will use a Solver to reason over our theory plus ground terms. We will use the Souffle solver

from typedlogic.registry import get_solver
solver = get_solver("souffle")
solver.add(theory)

model = solver.model()
n = 0
for t in model.iter_retrieve("CatOwner"):
    print(t)
    n += 1

CatOwner(Freddy)

assert n == 1