ryukinix / lisp-inference

An Inference Engine based on Propositional Calculus written in Common Lisp

Lisp Inference

A non-full featured Lisp Inference Engine because I didn't implemented the reductor yet. The algorithm commonly used it's the Wang Algorithm, maybe can you help me?

Usage

The main usage for now it's using as a truth-table generator by using its command line interface. You can download the last release and use as showed in the last picture as following:

ros install ryukinix/lisp-inference
~/.roswell/bin/inference

You need ros installed: Roswell

License

BSD

Author

Manoel Vilela

lisp-inference's Issues

Webapp doesn't handle parenthesis correctly

This occurs because my lexer it's just a split by whitespace. I need to fix that.

lisp-inference/web/webapp.lisp

Lines 37 to 41 in 3a51c46

	(defun parse-string (string)
	"Translate string to a list expression"
	(mapcar (lambda (x)
	(intern (string-upcase x) :lisp-inference))
	(str:words string)))

Fix problem about namespace issues on the printh-truth-table procedure

Because a problem of namespace operators defined inside of https://github.com/ryukinix/lisp-inference/blob/master/src/operators.lisp are not been catched as normal operators on the eval-operations function used in printh-truth-table. The strategy is to remap all the EXP car symbols to eventual symbols defined inside of :inference package, as defined a util function here:

lisp-inference/src/truth-table.lisp

Lines 155 to 157 in e2bf222

	(defun intern-symbol (s)
	"Get a internal symbol reference of S"
	(intern (symbol-name s) :lisp-inference))

Related to:

lisp-inference/src/truth-table.lisp

Lines 89 to 104 in e2bf222

	(defun eval-operations (exp-tree)
	"Generate all the truth-table cases and evaluated it based on EXP-TREE"
	(let ((cases (group-cases-to-propositions exp-tree)))
	(labels ((eval-expression (exp case)
	(loop for pair in case do
	(let ((prop (car pair))
	(value (cadr pair)))
	(nsubst value prop exp)))
	(eval exp)))
	(let ((exps (stack-of-expressions exp-tree)))
	(loop for case in cases
	collect (append case
	(loop for exp in exps
	collect (list exp
	(eval-expression (copy-tree exp)
	case)))))))))

The following images are examples of this bug occurying when we set different namespaces by (in-package :inference) or (in-package :cl-user)

Add implication equivalence

p => q <=> ~p v q

Refactor lisp-inference system

It's a little cumbersome, specially the truth-table module.

Beyond that I need to fix some misconceptions about handle multiple propositions and conjunctions. Mainly related to https://github.com/ryukinix/lisp-inference/blob/master/src/inferences.lisp

Rename: addiction -> addition

Addiction is a typo. Doesn't refer correctly to the proper inference rule addition.

Remove duplicates on stack-of-expressions

Possible Procedure related:

lisp-inference/src/truth-table.lisp

Line 75 in 0216fc3

(defun stack-of-expressions (exp)

Refactor string parser and lexer: mainly for webapp usage

• It should tokenize tokens first based on operations, supporting concatenated (without whitespaces) exps like this: p^q.
• It should use a LL(1) parser
• It should supports parenthesis without any problem
• It should fail early instead of trying be clever.

Example:

In: "p^q=>r" 
Out: (=> (^ p q) r)

Write unit-tests in the Common Lisp idiomatic way as ASDF system

Good resources: https://github.com/fare/asdf/blob/master/doc/best_practices.md

Implement Wang's Algorithm

This algorithm should takes N premises and one conclusion and check if the conclusion is valid.

Webapp should treat invalid expressions and avoid server kill or 500 HTTP errors

I need properly treat the invalid requests and show a proper message without letting the server die.

Add reader macro for proposition as P()

Whishful desires:

(prove :premises (list P(p => q) P(q))
       :conclusion P(q)) ;; T
;;; modus ponens

Create a web server + front to host lisp-inference

This should be simple and inspired in the project ultralisp.org

Create a parser for infix->prefix notation

This could be used as input of print-truth-table or another function to get a infix notation like p => (p ^ q) and translate to (=> p (^ p q ))

Setup Dockerfile + Travis CI

It should execute properly the unit tests. The ENTRYPOINT for the Dockerfile should be the inference-server running at port 40000.

Remove princ-n hack about print to *output-stream*

I should define a better way to print something to output-stream than calling (princ-n stuff)