PTR:

Background

Propositional Typicality Logic (PTL) is a newly proposed extension of Classical Propositional Logic with the addition of the typicality operator, $\bullet$. This operator represents the most typical situations in which a statement holds. Typicality allows for exceptions in propositional logic statements, with more expressivity than previous defeasible rules. With this, reasoning presents a new challenge. Entailment is the crux of reasoning in this setting. Two methods of entailment have been proposed for PTL: LM-Entailment and PT-Entailment.

The language of classical propositional logic consists of atoms representing true or false and boolean operators such as and, or, not and implication. Possible worlds are given by interpretations which assign a value of true or false to each atom, these valuations are what are used for entailment. Satisfying interpretations of a knowledge base are called a model. With the addition of the typicality operator, previous forms of entailment are no longer appropriate. In previous literature, 11 properties were propose that a form of entailment should entail for PTL. An impossibility result says that no form of entailment can satisfy all of them at once. Thus the two forms of entailment satisfy disjoint subsets of these properties.

Both forms of entailment use structures called ranked interpretations. These are rankings of valuations of a knowledge base with the lower levels representing the more typical worlds. Valuations not in the ranked interpretation are said to be on rank infinity. A ranked interpretation that satisfies a knowledge base is called a ranked model for that knowledge base.

Project Objectives

The goals of the project were to explore the theory of PTL and implement the algorithms for both forms of entailment as a Proof of Concept:

• To create an implementation of LM Entailment that matches the high level theoretical description from the literature
• To create an implementation of PT Entailment that matches the high level theoretical description from the literature

These implementations were then tested using toy examples.

Results

A successful proof of concept of the implementations of both LM-Entailment and PT-Entailment was produced. The entailment results and minimal models correctly matched the theoretical expectations. The results of each implementation were also compared against each other using toy examples.

Both algorithms were not computationally efficient, especially PT Entailment which explodes with the size of the knowledge base.