Propositional Logic | GameDev.net

I decided to make a simple Proposition Logic Theorem Prover type thing last night. Something I have wanted to do since I first took logic some years ago. Since it is propositional logic all statements are decidable via truthtables so its nothing fancy.

I wrote the interpreter in F#. F# has Fslex and Fsyacc tools that make language building quite easy. For example the AST is represented as:

 type expr =        | Val of string        | Bool of bool        | And of expr * expr        | Or of expr * expr        | Implies of expr * expr        | Not of expr         | Equiv of expr * expr//with where a some rules have been given to lexer e.g.:rule token = parse    | whitespace { token lexbuf }                             | newline    { (lexbuf: lexbuf).EndPos <- lexbuf.EndPos.NextLine; token lexbuf }       | "("        { LPAREN }    | ")"        { RPAREN }    | "^"        { AND }    | "Or"       { OR }    | "=>"       { IMPLIES }    .... //Or Parser :Expr: ID                      {  Val $1 }        | BOOL                    {  Bool $1 }    | Expr AND Expr           {  And ($1, $3) }    | Expr OR Expr            {  Or  ($1, $3) }    ...//And Interpreter in source via Match:let rec evalE (env: Mapbool>) = function    | Val v          -> if env.ContainsKey v then env.[v]                        else System.Console.WriteLine("\nDefaulting to true for unbound variable: " + v); true    | Bool b          -> b    | And  (e1, e2) -> evalE env e1 && evalE env e2  ....

The language is simple. It has only one type bool. Constants true and false which variable range over. There is assignment via sentences like:

raining := true; Cloudy := true; Shining := Not raining //You can then go something like"print (raining Or (Cloudy ^ Shining)) =>  (Not Shining ^ raining) Or (raining ^ Shining)"// to get err let me check ... trueAnother true prop:print (Cloudy ^ Shining) => (raining ^ Shining ^ Not Cloudy)

Cloudy and shining implies raining and shining and not cloudy.

If variables are not bound then true is simply used in place of identifier.

Expressions are combined with : ^ (and), => (implies), <=> (equivalence), Or, Not.

This is not useful. But it can print truthtables, check for tautologies, give counter examples, and list instances where a given formula hold. Variables here are need not bound since they are not searched for in the environment, they exist only to tell what to range over.

tautology p => q <=> p => q ^ q => p is given as true.

. That is all for now after a few hours work.

I wish to add:

pretty printing, strings and operations on strings, an interactive environment, simplification. Expression assignments. So I can go

Input: xorab = a Or Not b Or not b Or a; tautology a Or xorab  ^ p Or xorab

"EStore in pq exp p => q as true"; p := true. VStore p; tryprove q in pq

. Decided on simpler queries. e.g r := true. istrue q ^ p in p => q Or r. Simply breaks down expression after 'in' where searches for each in environment. else left alone. Then substitute each occurrence of bounded variables with values. Then for each variable after istrue extract table, if the union of all such vars is true then q ^ p is true. For example: in p ^ q Or r ^ q and defined r := true. Then it will tell you that q must also be true but p is unknown.

Modal logic would be fun to add although statements in modal logic are not decidable so it becomes a bit harder. But I can atleast do something like the raining example I gave but here it would be more helpful since it is more difficult to evaluate.

Discussion