#include "stdio.h" /* Formal Specification of Propositional Logic in C created 1998/04/08 modified 1998/06/14 */ /* infix 5 ==>; datatype formula = Pv of string | not of formula | op ==> of (formula * formula); */ enum formula_type {VAR, NEG, IMP}; typedef struct _formula { char type; // type of formula union { char* var; // used if type=VAR struct _formula* f; // used if type=NEG struct {struct _formula* antecedent; struct _formula* consequent; } i; // used if type=IMP } body; // "body" of formula } formula; int fsize= sizeof(formula); formula* Pv (char* variable_name) { formula* f = (formula*)malloc(fsize); f->type = VAR; f->body.var = variable_name; return f; } formula* Neg (formula* inf) { formula* negf = (formula*)malloc(fsize); negf->type = NEG; negf->body.f = (formula*)inf; return negf; } formula* Imp (formula* antf, formula* consqf) { formula* impf = (formula*)malloc(fsize); impf->type = IMP; impf->body.i.antecedent = antf; impf->body.i.consequent = consqf; return impf; } /* fun feval v (Pv s) = v s | feval v (not f) = if (feval v f)=true then false else true | feval v (f1 ==> f2) = if (feval v f1)=true then (feval v f2) else false; */ /* The following, though close to the ML, is almost certainly not the right way to do this in C, since the use of a function to represent the interpretation would be unsatisfactory. */ typedef enum {FALSE, TRUE} bool ; bool feval (const bool(*v)(char*), const formula* f) { switch (f->type) { case VAR : return (*v)(f->body.var); case NEG : return (feval(v, f->body.f) ? FALSE : TRUE); case IMP : return (feval(v, f->body.i.antecedent) ? feval(v, f->body.i.consequent) : TRUE); } }; /* abstype pthm = |- of formula with exception MpFail; fun MP (|- A) (|- (B ==> C)) = if A = B then |- C else raise MpFail | MP t1 t2 = t1; fun PS1 A B = |- (A ==> (B ==> A)); fun PS2 A B C = |- ((A ==>(B ==> C)) ==> ((A ==> B) ==>(A ==> C))); fun PS3 A B = |- ((not A ==> not B) ==> (B ==> A)); fun f (|- A) = A; end; */ /* The obvious way to do abstract data types is to use a C++ class. Since this is C I'll just use functions. We need an equality test over formulae. This comes free in ML but I don't think there is anything in C. */ typedef formula theorem; bool feq (formula* A, formula* B) { if ((A->type)==(B->type)) switch (A->type) { case VAR: return strcmp(A->body.var, B->body.var)?FALSE:TRUE; case NEG: return (feq (A->body.f, B->body.f)); case IMP: return (feq (A->body.i.antecedent, B->body.i.antecedent) && feq (A->body.i.consequent, B->body.i.consequent)); } else return FALSE; }; theorem* MP (theorem* A, theorem* B) { switch (B->type) { case IMP : if (feq (A, B->body.i.antecedent)) return B->body.i.consequent; }; return A; }; theorem* PS1 (formula* A, formula* B) {return Imp(A, Imp(B,A));}; theorem* PS2 (formula* A, formula* B, formula* C) { return Imp ( Imp(A, Imp(B, C)), Imp(Imp(A, B), Imp(A, C)) ); }; theorem* PS3 (formula* A, formula* B) {return Imp(Imp(Neg(A), Neg(B)), Imp(B, A));}; /* val f1 = (Pv "p") ==> (Pv "p"); (* this is the goal *) val L1 = PS1 (Pv "p") ((Pv "p") ==> (Pv "p")); val L2 = PS2 (Pv "p") ((Pv "p") ==> (Pv "p")) (Pv "p"); val L3 = MP L1 L2; val L4 = PS1 (Pv "p") (Pv "p"); val L5 = MP L4 L3; f1 = f L5; (* this checks that the result is the same as our goal *) */ main () { formula *p,*f1,*l1,*l2,*l3,*l4,*l5; bool r; p = Pv("p"); f1 = Imp(p,p); l1 = PS1 (p,Imp(p,p)); l2 = PS2 (p,(Imp(p,p)),p); l3 = MP (l1,l2); l4 = PS1 (p,p); l5 = MP (l4,l3); r = (feq (f1, l5)); printf (r ? "OK\n" : "FAILED\n"); }