AutoProof.Internal.Classical.SAT.TruthAssignment

Description

Defines the TruthAssignment class.

Synopsis

Documentation

Class representing truth assignments for evalutating propositional logic formulas.

Minimal complete definition

Methods

Evaluate the truth value of a variable under a given truth assignment.

Evaluate the truth value of a formula under a given truth assignment.

Instances details

TruthAssignment () a Source #	Assigns all propositional variables the truth value `False`. Can be used to evaluate closed formulas. Examples Expand `>>>` `() \|= (Var "a")`False `>>>` `() \|= (Or (Lit True) (Lit False))`True
Instance details Defined in AutoProof.Internal.Classical.SAT.TruthAssignment Methods evalVar :: () -> a -> Bool Source # evalFormula :: () -> Formula a -> Bool Source #
Ord a => TruthAssignment (Map a Bool) a Source #	Truth assignments where a missing key in the map is interpreted as `False`. Examples Expand `>>>` `t = Map.fromList $ [("a", True), ("b", False)]``>>>` `t \|= And (Var "a") (Not (Var "b"))`True `>>>` `t = Map.fromList $ [("a", True)]``>>>` `t \|= Imp (Var "a") (Var "b")`False
Instance details Defined in AutoProof.Internal.Classical.SAT.TruthAssignment Methods evalVar :: Map a Bool -> a -> Bool Source # evalFormula :: Map a Bool -> Formula a -> Bool Source #

Semantic entailment relation. This is an infix alias of evalFormula.

Expand

>>> t = Map.fromList $ [("a", True), ("b", False)]
>>> t |= And (Var "a") (Not (Var "b"))
True