A Calculator Machine for Logic

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.

  • A formula F is a logical consequence of a

Theory (knowledge base) T, i.e. T ⊨ F, if

all models of T are also models of F

  • Problem:
    • We have to consider all possible Interpretations
    • How do we do this in practice?
  • Therefore, logical consequence is implemented via syntactical methods (=Calculus).
  • For the logical calculus, there must be proven:
    • Correctness: every syntactic entailment is also a semantic entailment, if T ⊢ F then T ⊨ F
    • Completeness: all semantic entailments are also syntactic entailments, if T ⊨ F then T ⊢ F

Tags: machine, hypothesis, logic, inference
Parent: Logic

Update entry (Admin) | See changes

Comment on This Data Unit