Created on March 5, 2013, 11:30 p.m. by Hevok
& updated by
Hevok
on May 2, 2013, 5:30 p.m.

The Purpose is to build a Machine for Logic that is able to prove that a Logical Consequence is correct.

For a Formula F it can be said it is a logical consequence of a Theory or Knowledge Base, only if all Models of T are also Models of F, then F is a Consequence of T.

The problem is when one wants to build a machine to proof this, one has to consider all interpretations which takes a lot of time. In practice one does this by avoiding this.

So one need to create a mechanical method for solving logical Problems.

In order to this one has to come up with a syntactical method not a semantic method. One has to implement logical Consequence simply be a syntactical method, a so called Calculus. For this logical Calculus two things must be proven.
First the Correctness that every syntactic entailment also must be a semantic entailment. Vice versa one has to prove the Completeness that all Semantic Entailments on the same hand must be syntactic Entailments, then one can also use the syntactic Entailments method for the Semantic Entailment.

## Comment on This Data Unit