Sunday, February 17, 2013

Automated Proof Checking

Define a literal to be either an atomic sentence, or the negation of an atomic sentence. A model is the conjunction of literals so that a literal and its negation are not both in the model.  In existential graphs, a satisfaction graph is the disjunction of models, and looks like this (M_i represents a model):

In satisfaction graphs, you can think of a model as a possible assignment of variables that would make the graph true. It turns out that any existential graph can be converted into a satisfaction graph. If a graph is inconsistent, there can be no possible assignment of values that makes it true (i.e., no models). Therefore, the satisfaction graph for that graph would be an empty cut (or FALSE). Now assume we have two graphs, P and Q, and we'd like to show that Q follows from P. This is the same as saying that the graph conjuncting P and not Q yields a contradiction, and that the satisfaction graph for P and not Q is an empty cut. So, to test if P implies Q, we simply look at the satisfaction graph of P and not Q.

For more info on how to convert a graph into a satisfaction graph, look at:

No comments:

Post a Comment