5DV248 · Trustworthy Human-AI Interaction · Interactive laboratory

Lab 15 — Asking and Telling with First-Order Logic

Represent facts and general rules about a fictional university. Use predicates, variables and quantifiers to tell the knowledge base what is true, then ask what follows.

Intermediate · Knowledge representation · Interactive

Learning objectives

Teaching scenario: a fictional university. The domain and vocabulary are intentionally small so that students can inspect every inference.

1 · The formal language

We use a function-free, positive Horn fragment of first-order logic. Facts are ground atoms. Rules are universally quantified implications whose body is a conjunction of atoms and whose head is one atom. Function symbols, equality, negation, disjunction and existential rule heads are outside this laboratory's fragment.

Signature

\(\Sigma=(C,F,P)\)

\(C\): constants; \(F\): function symbols; \(P\): predicate symbols with specified arities.

\(C=\{alice,bob,ai,robotics\},\quad F=\varnothing\)
\(P=\{Student/1,Person/1,Course/1,EnrolledIn/2,Teaches/2,Lecturer/1\}\)

Knowledge base

\(\mathcal{K}=(\Sigma,\mathcal{F},\mathcal{R})\)

\(\mathcal{F}\): ground facts. \(\mathcal{R}\): universally quantified Horn rules.

A rule such as \(Student(x)\rightarrow Person(x)\) is shorthand for universal quantification over its variables.

Syntax used in this laboratory

ExpressionMeaningExample
\(P(a)\)Unary predicate applied to a constant\(Student(alice)\)
\(R(a,b)\)Binary predicate applied to two constants\(EnrolledIn(alice,ai)\)
\(\forall x\,\varphi\)For every domain element, \(\varphi\) holds\(\forall x(Student(x)\to Person(x))\)
\(\exists x\,\varphi\)There is at least one domain element satisfying \(\varphi\)\(\exists x(Student(x)\land EnrolledIn(x,ai))\)
\(\varphi\land\psi\)Both formulas hold\(Student(x)\land EnrolledIn(x,ai)\)
\(\varphi\to\psi\)If \(\varphi\), then \(\psi\)\(Student(x)\to Person(x)\)

Semantics: interpretations and satisfaction

\(\mathcal{M}=(\Delta^\mathcal{M},\cdot^\mathcal{M})\)

An interpretation has a non-empty domain \(\Delta^\mathcal{M}\), maps each constant to a domain element, and maps each n-ary predicate to an n-ary relation over that domain.

\(\mathcal{M}\models P(a)\iff a^\mathcal{M}\in P^\mathcal{M}\)
\(\mathcal{M},g\models P(x)\iff g(x)\in P^\mathcal{M}\)
\(\mathcal{M},g\models\forall x\,\varphi\iff\text{for every }d\in\Delta^\mathcal{M},\;\mathcal{M},g[x\mapsto d]\models\varphi\)
\(\mathcal{M},g\models\exists x\,\varphi\iff\text{for some }d\in\Delta^\mathcal{M},\;\mathcal{M},g[x\mapsto d]\models\varphi\)

Here, \(g\) is a variable assignment. A sentence has no free variables. The symbols \(\forall\) and \(\exists\) quantify over the interpretation's domain, not merely over the names displayed in the interface.

2 · Start with a knowledge base

The initial facts and rules are shown below. A rule is written in the interface using ^ for conjunction and -> for implication; all variables in a rule are implicitly universally quantified.

Facts · Ground atoms
Student(alice)
Student(bob)
Course(ai)
Course(robotics)
EnrolledIn(alice, ai)
EnrolledIn(bob, robotics)
Lecturer(mira)
Teaches(mira, ai)
Rules · Universally quantified
Student(?x) -> Person(?x)
Lecturer(?x) -> Person(?x)
Student(?x) ^ EnrolledIn(?x, ?c) -> ActiveStudent(?x)
Lecturer(?x) ^ Teaches(?x, ?c) -> TeachingStaff(?x)

Variables beginning with ? are universally quantified over the rule.

For example, the first rule and Student(alice) entail Person(alice). The third rule and Alice's enrolment entail ActiveStudent(alice).

3 · TELL — Add facts and rules

Add a ground atom or a universally quantified Horn rule. Use declared constants and predicate names. Predicate arity must remain consistent.

Choose a statement and add it to the knowledge base.

Current knowledge base

Facts
Rules
Input syntax and restrictions

Atoms have the form Predicate(constant) or Predicate(constant, constant). Rules have the form Atom ^ Atom -> Atom. Use variables such as ?x. Every variable in the rule head must also occur in its body (range restriction). Rule bodies and heads contain positive atoms only. Constants are treated as distinct names in this finite implementation.

4 · ASK — Query the knowledge base

Ask a ground atomic query, or an existential conjunctive query. Existential queries search for a variable assignment that makes every atom in the conjunction true.

Submit a query to see the result.

Query explanation

No query has been evaluated yet.
Try these queries
  • Person(alice) — should succeed by applying a rule.
  • ActiveStudent(bob) — should succeed using Bob's enrolment.
  • TeachingStaff(mira) — should succeed using the teaching rule.
  • Student(mira) — should not be derived; this does not prove its negation.
  • Student(?x) ^ EnrolledIn(?x, ai) — should return Alice as a witness.
  • Person(?x) ^ EnrolledIn(?x, ?c) — should return matching bindings for people and courses.

5 · Inference — From facts to consequences

The engine repeatedly applies rules to known facts until no new ground atom can be added. The resulting set is the least Herbrand model of this function-free, range-restricted positive Horn program over the constants in the knowledge base.

Asserted facts

Derived facts

Run inference to display derived facts.

No inference run yet.

6 · Mathematical view of entailment

A sentence is entailed when it is true in every model of the knowledge base:

\(\mathcal{K}\models\varphi\quad\text{iff}\quad\forall\mathcal{M}\;(\mathcal{M}\models\mathcal{K}\Rightarrow\mathcal{M}\models\varphi)\)

For this positive function-free Horn fragment, the least Herbrand model provides a canonical model for answering ground atomic and positive existential conjunctive queries.

\(\mathcal{H}_{\mathcal{K}}=(C,\{P(t_1,\ldots,t_n)\mid P(t_1,\ldots,t_n)\text{ is in the closure}\})\)
\(\mathcal{K}\models A\quad\text{iff}\quad A\in\operatorname{LM}(\mathcal{K})\)

For a conjunctive query \(Q=\exists\vec{x}(A_1\land\cdots\land A_n)\), the query succeeds when there is a substitution \(\theta\) for its variables such that every instantiated atom \(A_i\theta\) belongs to the least-model closure.

What this implementation computes

The engine computes a finite forward-chaining closure for positive, function-free, range-restricted Horn rules. It supports ground atomic queries and positive existential conjunctive queries. It does not implement unrestricted FOL, arbitrary quantifier alternation, negation, disjunction, equality, function symbols, existential rule heads, or a general-purpose FOL theorem prover. The finite set of constants is treated under a unique-name convention; this is an implementation choice, not a universal assumption of FOL semantics.

7 · Check your understanding

Question 1

What is the arity of EnrolledIn(alice, ai)?

Question 2

What does the rule Student(?x) -> Person(?x) mean?

Question 3

If Student(mira) is not derived, can we conclude ¬Student(mira)?