HasKLM

Hasklm is a Haskell based defeasible reasoner using the KLM-approach.

Features

Overview Feature List:

Parsing a string into a propositional formula.
Computation of the valuations/models for propositional knowledge bases.
Propositional satisfiability checking.
Propositional entailment checking.
The Base Rank algorithm.
Rational Closure based defeasible entailment checking.

Planned Feature List:

Lexicographic Closure based defeasible entailment checking.
Rigorous testing.
The Relevant Closure algorithm.
Propositional knowledge base parsing.
Defeasible implication parsing.
Defeasible knowledge base parsing.
Joint knowledge base parsing.
Knowledge base generation.

Checkout the docs for all currently available functionality.

Usage

Stack is the project's build tool.

Commonly Used Commands:

Build Project:

stack build

Run Tests:

stack test

Load All Modules into GHCi (For Development/Testing purposes):

stack repl

Load Application into GHCi:

stack repl --only-main

Examples

Examples can be found in the test file.

RationalClosure Example

This example will be in reference to the birds and penguins classical reasoning problem.

Instructions

Load the application.

stack repl --only-main

Define the defeasible implications.

let defImpl1 = typically (str2form "bird Implies flies")
let defImpl2 = typically (str2form "bird Implies wings")
let defImpl3 = typically (str2form "penguin Implies Not flies")

Construct a defeasible knowledge base using the defeasible implications.

let dkb = [defImpl1, defImpl2, defImpl3]

Define the classical propositional formulas.

let propForm1 = str2form "penguin Implies bird"
let propForm2 = str2form "Robin Implies bird"

Define the propositional knowledge base.

let pkb = [propForm1, propForm2]

Combine the propositional and defeasible knowledge bases into a joint knowledge base relation.

let jkb = (pkb, dkb)

Define a defeasible query.

let defQuery = typically (str2form "penguin Implies bird")

Execute Rational Closure defeasible entailment checking with the joint knowledge base and defeasible query, printing the result.

print (entailsRC jkb defQuery)

If the above outputs True, all is well! A penguin is still a bird! For interests sake, we will define another defeasible query.

let defQuery2 = typically (str2form "penguin Implies wings")

Execute and print as before.

print (entailsRC jkb defQuery2)

If the above outputs False, all is still well! Rational Closure concludes that since penguins are atypical birds that do not fly, it is most likely that penguins do not have wings either.

Disclaimer

I am still quite a novice when it comes to formalised logic. I've tried to define everything using names that closely relate to their corresponding concepts in formal KRR literature, mostly in reference to Adam Kaliski's 2020 Dissertation on the topic. Some (if not most) of the functions and procedures are not as efficient as they could be, but that's just the nature of programming isn't it.

With that being said, I am open to any and all suggestions in order to improve the repo, whether they pertain to readability, efficiency, functionality, Haskell best practices, or just to give it better relations to the literature.