> module Prop where
> import Data.Map (Map)
> import qualified Data.Map as Map
> import Data.List (find,nub)
===================
(1) Syntax of Prop
===================
Let variables be strings in our case.
> type Variable = String
Syntax of propositional logic, given by:
> data PropFormula
> = And PropFormula PropFormula
> | Or PropFormula PropFormula
> | Impl PropFormula PropFormula
> | Not PropFormula
> | FTrue | FFalse
> | Var Variable
Further logical connectives can be defined from these,
e.g. have
> iff :: PropFormula -> PropFormula -> PropFormula
> iff a b = And (Impl a b) (Impl b a)
for the <=> connective (if-and-only-of).
Note that not all fixed connectives are needed: Impl and And can easily be
defined in terms of Or and Not.
======================
(2) Semantics of Prop
======================
> type Tr = Bool
Hence, the set of "truth values" Bool = {True, False} is the
set of denotations for the propositional formulas.
====================================
(3) Connecting Syntax with Semantics
====================================
A "valuation" is a mapping that assigns each variable a value from {True, False}.
Its type is given by:
> type Valuation = Map Variable Tr
In order to create such a valuation, we need to find out what variables are
inside of the formula. This can be done, e.g., via
> vars :: PropFormula -> [Variable]
> vars (And f1 f2) = nub $ (vars f1) ++ (vars f2)
> vars (Or f1 f2) = nub $ (vars f1) ++ (vars f2)
> vars (Impl f1 f2) = nub $ (vars f1) ++ (vars f2)
> vars (Not f1) = vars f1
> vars (Var v) = [v]
> vars _ = []
A formula that contains no variables is called "ground".
> ground :: PropFormula -> Bool
> ground = null . vars
Example:
The formula
"a" && "b"
contains two variables, hence it is not ground.
A suitable valuation could be:
a -> True
b -> True
If the formula contains n variables, there are 2^n possible valuations.
These valuations can be computed by the following routine:
> allVals :: [Variable] -> [Valuation]
> allVals [] = [Map.empty]
> allVals (v:vs) = let cs = allVals vs in
> map (Map.insert v True) cs ++ map (Map.insert v False) cs
An "evaluation" of a formula with respect to a valuation v is simply
the truth value of that formula when all variables are substituted by their
according truth value. This is actually the valuation mapping from above
extended to propositional formulas.
> eval :: Valuation -> PropFormula -> Tr
> eval v (And f1 f2) = eval v f1 && eval v f2
> eval v (Or f1 f2) = eval v f1 || eval v f2
> eval v (Impl f1 f2)= not (eval v f1) || eval v f2
> eval v (Not f) = not $ eval v f
> eval _ FTrue = True
> eval _ FFalse = False
> eval v (Var var) = case Map.lookup var v of
> Just x -> x
> Nothing -> error $ "No Variable '"++var++"' found in Context"
=========================
(4) Important Definitions
=========================
There are types of formulas that have special attention:
A formula f is called "satisfiable" if and only if there is one valuation v such that
f evaluates to True with respect to valuation v (in short: eval v f == True).
This can be expressed by
> satisfiable :: PropFormula -> Bool
> satisfiable f = any (\ v -> eval v f ) (allVals $ vars $ f)
A formula f is called a "contradiction" if and only if there is no valuation v such that
f evaluates to True with respect to valuation v (in short: eval v f == False, for all valuations v).
This can be expressed by
> contradiction :: PropFormula -> Bool
> contradiction = not . satisfiable
A formula f is called "valid" or "theorem" if and only if it evaluates to True *for all*
possible valuations v. This is denoted |= f.
> valid :: PropFormula -> Bool
> valid f = all (\ v -> eval v f ) (allVals $ vars $ f)
Two important logical relations between formulas are:
1) Entailment
A formula f1 entails a formula f2 iff the formula "f1 => f2" is valid.
> entails :: PropFormula -> PropFormula -> Bool
> entails f1 f2 = contradiction ( And f1 (Not f2) )
2) Equivalence
Two formulas are equivalent if both of them are True resp. False for the same
valuations.
> equiv :: PropFormula -> PropFormula -> Bool
> equiv f1 f2 = f1 `entails` f2 && f2 `entails` f1
===========
(5) Calculi
===========
A calculus is a syntactic procedure that allows us to derive the truthhood or falsity
or a formula without using semantic evaluation.
A calculus is essentially a function "proves" that has the same signature as "valid", hence
> proves :: PropFormula -> Bool
> proves = undefined
If, for a function f, "proves f" is True, we call the formula "provable", written |- f.
There are two major properties for any proof calculus:
(1) If from |- f it follows that |= f, then the calculus is called "sound"
(2) If from |= f it follows that |- f, then the calculus is called "complete".
========================================
Further stuff ...
> modelsOf :: PropFormula -> [Valuation]
> modelsOf f = filter (\c -> (eval c f)) $ allVals $ vars f
> modelOf :: PropFormula -> Maybe Valuation
> modelOf = foldr (\a b -> Just a) Nothing . modelsOf
> instance Show PropFormula where
> show (And f1 f2) = "("++show f1++" && "++show f2++")"
> show (Or f1 f2) = "("++show f1++" || "++show f2++")"
> show (Impl f1 f2) = "("++show f1++" => "++show f2++")"
> show (Not f) = "~("++show f++")"
> show (FTrue) = "True"
> show FFalse = "False"
> show (Var v) = v
> instance Eq PropFormula where
> (==) = equiv