This repository contains software developed as part of the dissertation 'Implementation and Evaluation of KLM-Style Defeasible Entailment and Explanation Algorithms', submitted in fulfilment of the requirements for the degree of Master of Science in the Department of Computer Science, Faculty of Science, University of Cape Town.
klm-algorithms is a modular software tool for computing defeasible entailment and justification-based explanations within the Kraus–Lehmann–Magidor (KLM) framework for non-monotonic reasoning. The tool implements the three principal KLM inference operators, Rational Closure, Lexicographic Closure, Basic Relevant Closure, and Minimal Relevant Closure, together with multiple optimised algorithmic variants for each operator.
The system provides a unified environment for:
- Constructing and editing propositional defeasible knowledge bases
- Defining defeasible statements
- Computing defeasible consequences under different KLM inference strategies
- Generating minimal justification sets, explaining why each conclusion holds
- Comparing algorithmic behaviour across operators and datasets
In addition to operator-specific justification procedures, the tool includes a universal justification algorithm that extracts all justifications from any deciding knowledge base, regardless of the inference operator that generated it.
Designed for both researchers and practitioners, KLM-Algorithms supports reproducible experimentation, scalable testing on synthetic and benchmark datasets, and visual exploration of entailments and explanations. It aims to provide a practical, extensible platform for studying defeasible reasoning, evaluating reasoning algorithms, and developing explainable AI systems grounded in formal logic.
- Maven 4.0+
- Java 21+
There's a binary under app/ folder which can be run without need for compilation. However, it still requires Java 21+. To run the binary run java -jar app/klm-algorithms-1.0-SNAPSHOT.jar and go to http://localhost:8080/.
mvn clean packagejava -jar target/klm-algorithms-1.0-SNAPSHOT.jarAfter running the above command, visit http://localhost:8080/ on your web browser. Check the syntax before sending the queries.
Alternately, you can just access the live web deployement at https://klm-algorithms.fly.dev.
- Chipo Hamayobe (chipo@cs.uct.ac.za) - Project Lead
-
The TweetyProject - http://tweetyproject.org
The TweetyProject consists of diverse Java libraries that embody strategies for knowledge representation formalisms, encompassing classical logics, conditional logics, and probabilistic logics.
-
The SAT4J SAT Solver - http://www.sat4j.org
The SAT4J SAT Solver is a Java library designed to solve problems related to boolean satisfaction and optimisation.
-
JUnit - https://junit.org
The JUnit is a widely adopted open-source framework that provides a structured and organised approach to writing and running unit tests in Java applications.