george: User Manual

[ Introduction ] [ File Structure ] [ #check PROP ] [ #check PRED ] [ #check PREDTYPES ] [ #check SEM (etc) ] [ #check TP ]
[ #check ND ] [ #check ST ] [ Arithmetic ] [ Sets ] [ #check Z ] [ #check PC ]
[ Contributions by Students ] [ Credits ] [ Keywords ]

Evaluating Boolean Valuations/Interpretations (#check SEM/SEM_SAT/SEM_CONSISTENT/SEM_F/SEM_T/SEM_CE)

There are several george commands (SEM/SEM_SAT/SEM_CONSISTENT/SEM_F/SEM_T/SEM_CE) that evaluate formulas in a Boolean valuation (for propositional logic) or an interpretation (for predicate logic).

All of these commands take a BV or an interpretation plus a formula, a set of formulas, or an argument and then check if the formula(s)/argument is satisfiable, false, consistent, etc.

A BV is described as: 

[a:bool] := T
[b:bool] := F
[c:bool] := F

Note that T and F must be used for truth values in a Boolean valuation.

An untyped interpretation is described as: 

[univ] := {d1, d2}
[p:univ --> bool] := {(d1, T), (d2, T)}

A typed interpretation is described as: 

[D] := {d1, d2}
[E] := {e1}
[p: E prod D --> bool] := {(e1, d1,F), (e1, d2,T)}

The command #check SEM gives a response that is the meaning of the formula in the provided BV/interpretation. 

#check SEM

[a:bool] := T
[b:bool] := F

a => b

// result
// ++ Comment: Formula means F


#check SEM

[univ] := {d1, d2}
[p:univ --> bool] := {(d1, T), (d2, T)}

forall x:univ. p(x)

// result:
// ++ Comment: Formula means T

Here are examples of each of the other commands in a mixture of propositional logic and untyped and typed predicate logic: 

#check SEM_SAT

[a:bool] := T
[b:bool] := F
[c:bool] := F

a & b => c

// result:
// ++ Comment: Formula means T
// ++ Comment: BV/Interpretation has the correct meaning


#check SEM_SAT

[a:bool] := T
[b:bool] := T
[c:bool] := F

a & b => c 

// result:
// ++ Comment: Formula means F
// -- Error: Formula does not mean T in this BV/interpretation


#check SEM_SAT

[univ] := {d1, d2}
[p: univ --> bool] := {(d1,T),(d2,T)}

forall x. p(x)

// result:
// ++ Comment: Formula means T
// ++ Comment: BV/Interpretation has the correct meaning


#check SEM_SAT

[D] := {d1, d2}
[E] := {e1}
[p: E prod D --> bool] := {(e1, d1,F), (e1, d2,T)}

forall e: E . exists d:D . p(e,d)

// result:
// ++ Comment: Formula means T
// ++ Comment: BV/Interpretation has the correct meaning


#check SEM_F

[univ] := {d1, d2}
[p: univ --> bool] := {(d1,F),(d2,T)}

forall x. p(x)

// result:
// ++ Comment: Formula means F
// ++ Comment: BV/Interpretation has the correct meaning


#check SEM_T

[univ] := {d1, d2}
[p: univ --> bool] := {(d1,F),(d2,T)}

forall x. p(x)

// result:
// ++ Comment: Formula means F
// -- Error: Formula does not mean T in this BV/interpretation


#check SEM_CONSISTENT

[a:bool] := T
[b:bool] := F

a | b, b => a

// result:
// ++ Comment: Formula 1 means T
// ++ Comment: Formula 2 means T
// ++ Comment: BV/Interpretation has the correct meaning


#check SEM_CONSISTENT

[univ] := {d1, d2}
[p:univ --> bool] := {(d1, F), (d2, T)}

forall x:univ. p(x),
exists x:univ. p(x)

// result:
// ++ Comment: Formula 1 means F
// ++ Comment: Formula 2 means T
// -- Error: Formulas do not all mean T in this BV/interpretation


#check SEM_CE

[a:bool] := F
[b:bool]:= T

b & a |- a

// result:
// ++ Comment: Premise 1 means F
// ++ Comment: Conclusion means F
// -- Error: Not a counterexample to this argument

What does george check?

For evaluation questions, george checks: