kb |= q?

This is an inference engine tool based on propositional logic.

Given a knowledge base kb with a set of statements, the inference engine is capable of telling if a given statement q is entailed by the knowledge base.

Basically, the engine checks if kb |= q

Usage:

Build and Run

The project uses Cabal for building. You can build it using:

cabal build

To run the executable:

cabal run logic-inference <filepath> --algorithm <v1/v2/v3>

--algorithm is an optional flag. By default, v1 is used.

File template

The program accepts input files in a simple text format. Here's an example (modus ponens):

p = "It is raining"
q = "The ground is wet"

knowledge[
    p -> q
    p
]

query[
    q
]

File Format:

• Variables can be defined with descriptions using variable = "description"
• The knowledge[] block contains the knowledge base statements
• The query[] block contains the query statement

Note on Parser: The parser is intentionally kept simple for readability. It expects one statement per line and proper spacing around operators. Comments and empty lines are ignored.

Note: the current V2 is an incomplete algorithm as it's not deriving all possible conclusions from inference rules.

So it might return false negatives!

Tests

In a similar manner, instead of testing with executing the program, you can simply add some tests to tests/InferenceSpec.hs

v1: Recursive enumeration and validation of models

A recursive algorithm that, enumerating all models given knowledge base's (kb) and query's (q) symbols, checks if for all models in which the knowledge base is true, if query q is also true for the given model.

Time complexity: O(2^n) in which n equals the number of symbols in kb U q.

Example:

Modus Ponens

knowledge[
    p -> q
    p
]

query[q]

Enumerate all possible models:

| p | q | kb |
|---|---|----|
| T | T | T  | # the only true model
| T | F | F  | # modus ponens, true -> q, therefore q must be also true. Invalid model
| F | T | F  | # p is true on the kb, so this model is invalid
| F | F | F  | # p is true on the kb, so this model is invalid

For all models in which kb is true, meaning just one of the models, is the query (q=q) also true? Yes, q is true for this model, therefore kb entails q.

v2: Search by inference rules

Given the initial knowledge base, new propositions will be generated by inference rules upon the already existent information. The new propositions will be added to the knowledge base.

The algorithm will then check if the query's proposition is within the knowledge base. If not, it continues to apply inference rules, now using also the new propositions included to the knowledge base.

If the query's proposition is within the knowledge base, then kb entails q.

Otherwise, after applying all possible inference rules, if the knowledge base does not contain the query's proposition, then kb does not entail q.

Types of inference rules to be applied:

• Immediate inference: applied upon one proposition
• Syllogisms: applied upon two propositions
• Compound syllogisms: applied upon three or more propositions

The algorithm will only be complete if it derives all possible conclusions from all possible inference rules recursively (considering new propositions added along the way).

Otherwise, it will return false negatives.

Can we we even enumerate all possible inference rules anyway?

v3: Search by inference rules with, as last resource, recursive enumeration

First check for V2, if it returns false for kb |= q, then apply V1.

My current implementation of V2 is inefficient so it doesn't make sense to use V3 for now.

v4: Contradiction by Resolution

Convert all knowledge base's propositions to the Conjunctive Normal Form (CNF), apply resolution inference rule, removing the complementary litterals and finally try to find a contradiction.

Basically:

CNF(kb) AND CNF(~q)

TODO: implement it

vfinal: algorithm(s) selection by heuristics

The engine could smartly check when to use one algorithm or another, or different combinations of them.

Example: Supposing a knowledge base has more than 20 symbols, the engine would use probably use v2 + v3 as v1 would take 2^20 iterations to enumerate all models in the worst case scenario.

TODOs

• Algorithm v3: Resolution algorithm
• Algorithm v1: improvements (see TODOs on src/V1.hs)
• Algorithm v2: improvements (see TODOs on src/V2.hs)
• (maybe) Parser: use yaml instead of txt