I need to bulid an application in Prolog capable of loading a set of specified facts and/or rules supplied in a list (allow lists to come from files or supplied via a predicate call) and then internally store these facts/rules in relevant structures so that the system can answer queries passed to it. The application has to be able to produce a proof tree showing the entire reasoning behind a conclusion.

It must also provide an efficient front-end providing meaningful feedback for debugging purposes. it must implement the various rules of logic such as implication and its various related rules such as contrapositive, converse and inverse, elimination, introduction etc. The system also needs to tag the confidence in an outcome. Where the outcome is sound tag identify as sound, where an outcome is unsound or derived from any unsound ancestor it must be identified, this is similar to confidence levels in expert systems.

The following syntax will be used to pass operator logic into the system [Operator,Operand1, Operand2...Operandn]

Implies [=>,a,b]

And [*, a,b,c]

Or [*, a,b,c]

Compound Negation ~[*,a,b,c]

Unary negation is represented by ~ as in ~a or using brackets as necessary ~(~a)

has anyone any ideas

Are you familiar with Prolog? While I'm not an experienced Prolog programmer or
anything, I do know something about how it operates and the theory behind resolution
theorem proving. You can't represent just any logical statement in Prolog, the rule format
for Prolog is what is called a Horn Clause. These special class of clauses can be resolved in
Polynomial time, as opposed to the general class of SAT problems. So if you want to build
an expert system theorem prover, first you have to consider what is it you want to prove?
Not everything can be expressed in Prolog, so you should take that into consideration.

-Jeffery

................