Data.Logic.ATP.Prop

Description

Basic stuff for propositional logic: datatype, parsing and printing. IsPropositional is a subclass of IsLiteral of formula types that support binary combinations.

Synopsis

Propositional formulas

class IsLiteral formula => IsPropositional formula where Source #

A type class for propositional logic. If the type we are writing an instance for is a zero-order (aka propositional) logic type there will generally by a type or a type parameter corresponding to atom. For first order or predicate logic types, it is generally easiest to just use the formula type itself as the atom type, and raise errors in the implementation if a non-atomic formula somehow appears where an atomic formula is expected (i.e. as an argument to atomic or to the third argument of foldPropositional.)

Minimal complete definition

Methods

(.|.) :: formula -> formula -> formula infixl 4 Source #

Disjunction/OR

(.&.) :: formula -> formula -> formula infixl 5 Source #

Conjunction/AND. x .&. y = (.~.) ((.~.) x .|. (.~.) y)

(.<=>.) :: formula -> formula -> formula infixl 2 Source #

Equivalence. x .=. y = (x .=>. y) .&. (y .=>. x)

(.=>.) :: formula -> formula -> formula infixr 3 Source #

Implication. x .=>. y = ((.~.) x .|. y)

foldPropositional' :: (formula -> r) -> (formula -> BinOp -> formula -> r) -> (formula -> r) -> (Bool -> r) -> (AtomOf formula -> r) -> formula -> r Source #

A fold function that distributes different sorts of formula to its parameter functions, one to handle binary operators, one for negations, and one for atomic formulas. See examples of its use to implement the polymorphic functions below.

foldCombination :: (formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> formula -> r Source #

An alternative fold function for binary combinations of formulas

Instances

 IsAtom atom => IsPropositional (PFormula atom) Source # Methods(.|.) :: PFormula atom -> PFormula atom -> PFormula atom Source #(.&.) :: PFormula atom -> PFormula atom -> PFormula atom Source #(.<=>.) :: PFormula atom -> PFormula atom -> PFormula atom Source #(.=>.) :: PFormula atom -> PFormula atom -> PFormula atom Source #foldPropositional' :: (PFormula atom -> r) -> (PFormula atom -> BinOp -> PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r Source #foldCombination :: (PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> PFormula atom -> r Source # (IsFormula (QFormula v atom), HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsPropositional (QFormula v atom) Source # Methods(.|.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source #(.&.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source #(.<=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source #(.=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source #foldPropositional' :: (QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r Source #foldCombination :: (QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> QFormula v atom -> r Source #

data BinOp Source #

This type is used to construct the first argument of foldPropositional.

Constructors

 (:<=>:) (:=>:) (:&:) (:|:)

Instances

 Source # Methods Source # Methodssucc :: BinOp -> BinOp #pred :: BinOp -> BinOp #toEnum :: Int -> BinOp #enumFrom :: BinOp -> [BinOp] #enumFromThen :: BinOp -> BinOp -> [BinOp] #enumFromTo :: BinOp -> BinOp -> [BinOp] #enumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp] # Source # Methods(==) :: BinOp -> BinOp -> Bool #(/=) :: BinOp -> BinOp -> Bool # Source # Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BinOp -> c BinOp #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BinOp #dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BinOp) #dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp) #gmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r #gmapQ :: (forall d. Data d => d -> u) -> BinOp -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> BinOp -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # Source # Methods(<) :: BinOp -> BinOp -> Bool #(<=) :: BinOp -> BinOp -> Bool #(>) :: BinOp -> BinOp -> Bool #(>=) :: BinOp -> BinOp -> Bool #max :: BinOp -> BinOp -> BinOp #min :: BinOp -> BinOp -> BinOp # Source # MethodsshowsPrec :: Int -> BinOp -> ShowS #show :: BinOp -> String #showList :: [BinOp] -> ShowS #

binop :: IsPropositional formula => formula -> BinOp -> formula -> formula Source #

Combine formulas with a BinOp, for use building the first argument of foldPropositional.

(⇒) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #

Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.

(==>) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #

Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.

(⊃) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #

Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.

(→) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #

Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.

(⇔) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #

If-and-only-if synonyms

(<=>) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #

If-and-only-if synonyms

(↔) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #

If-and-only-if synonyms

(<==>) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #

If-and-only-if synonyms

(∧) :: IsPropositional formula => formula -> formula -> formula infixl 5 Source #

And/conjunction synonyms

· :: IsPropositional formula => formula -> formula -> formula infixl 5 Source #

And/conjunction synonyms

(∨) :: IsPropositional formula => formula -> formula -> formula infixl 4 Source #

Or/disjunction synonyms

Arguments

 :: JustPropositional pf => (pf -> BinOp -> pf -> r) fold on a binary operation formula -> (pf -> r) fold on a negated formula -> (Bool -> r) fold on a boolean formula -> (AtomOf pf -> r) fold on an atomic formula -> pf -> r

Deconstruct a JustPropositional formula.

Arguments

 :: (JustPropositional pf1, JustPropositional pf2) => (pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r) Combine two binary operation formulas -> (pf1 -> pf2 -> Maybe r) Combine two negated formulas -> (Bool -> Bool -> Maybe r) Combine two boolean formulas -> (AtomOf pf1 -> AtomOf pf2 -> Maybe r) Combine two atomic formulas -> pf1 -> pf2 -> Maybe r Result is Nothing if the formulas don't unify

Combine two JustPropositional formulas if they are similar.

Arguments

 :: (JustPropositional pf1, IsPropositional pf2) => (AtomOf pf1 -> AtomOf pf2) Convert an atomic formula -> pf1 -> pf2

Convert any instance of JustPropositional to any IsPropositional formula.

Arguments

 :: (IsPropositional formula, JustPropositional pf) => (formula -> pf) Convert a higher order formula -> (AtomOf formula -> AtomOf pf) Convert an atomic formula -> formula -> pf

Convert any instance of IsPropositional to a JustPropositional formula. Typically the ho (higher order) argument calls error if it encounters something it can't handle.

Implementation of precedence for any JustPropostional type.

prettyPropositional :: forall pf. JustPropositional pf => Side -> PrettyLevel -> Rational -> pf -> Doc Source #

Implementation of pPrint for any JustPropostional type.

showPropositional :: JustPropositional pf => Side -> Int -> pf -> ShowS Source #

Implementation of show for any JustPropositional type. For clarity, show methods fully parenthesize

onatomsPropositional :: JustPropositional pf => (AtomOf pf -> AtomOf pf) -> pf -> pf Source #

Implementation of onatoms for any JustPropositional type.

overatomsPropositional :: JustPropositional pf => (AtomOf pf -> r -> r) -> pf -> r -> r Source #

Implementation of overatoms for any JustPropositional type.

Restricted propositional formula class

class IsPropositional formula => JustPropositional formula Source #

Class that indicates a formula type *only* supports Propositional features - it has no way to represent quantifiers.

Instances

 IsAtom atom => JustPropositional (PFormula atom) Source #

Interpretation of formulas.

eval :: JustPropositional pf => pf -> (AtomOf pf -> Bool) -> Bool Source #

Interpretation of formulas.

atoms :: IsFormula formula => formula -> Set (AtomOf formula) Source #

Return the set of propositional variables in a formula.

Truth Tables

data TruthTable a Source #

Constructors

 TruthTable [a] [TruthTableRow]

Instances

 Eq a => Eq (TruthTable a) Source # Methods(==) :: TruthTable a -> TruthTable a -> Bool #(/=) :: TruthTable a -> TruthTable a -> Bool # Show a => Show (TruthTable a) Source # MethodsshowsPrec :: Int -> TruthTable a -> ShowS #show :: TruthTable a -> String #showList :: [TruthTable a] -> ShowS # Pretty atom => Pretty (TruthTable atom) Source # MethodspPrintPrec :: PrettyLevel -> Rational -> TruthTable atom -> Doc #pPrint :: TruthTable atom -> Doc #pPrintList :: PrettyLevel -> [TruthTable atom] -> Doc #

onallvaluations :: Ord atom => (r -> r -> r) -> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r Source #

truthTable :: JustPropositional pf => pf -> TruthTable (AtomOf pf) Source #

Code to print out truth tables.

Tautologies and related concepts

tautology :: JustPropositional pf => pf -> Bool Source #

Recognizing tautologies.

unsatisfiable :: JustPropositional pf => pf -> Bool Source #

Related concepts.

Substitution

psubst :: JustPropositional formula => Map (AtomOf formula) formula -> formula -> formula Source #

Substitution operation.

Dualization

dual :: JustPropositional pf => pf -> pf Source #

Dualization.

Simplification

psimplify :: IsPropositional formula => formula -> formula Source #

Routine simplification.

psimplify1 :: IsPropositional formula => formula -> formula Source #

Normal forms

nnf :: JustPropositional pf => pf -> pf Source #

Negation normal form.

nenf :: IsPropositional formula => formula -> formula Source #

list_conj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula Source #

Disjunctive normal form (DNF) via truth tables.

list_disj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula Source #

mk_lits :: (JustPropositional pf, Ord pf) => Set pf -> (AtomOf pf -> Bool) -> pf Source #

allsatvaluations :: Ord atom => ((atom -> Bool) -> Bool) -> (atom -> Bool) -> Set atom -> [atom -> Bool] Source #

dnfSet :: (JustPropositional pf, Ord pf) => pf -> pf Source #

purednf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #

simpdnf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #

With subsumption checking, done very naively (quadratic).

rawdnf :: IsPropositional formula => formula -> formula Source #

dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf Source #

Mapping back to a formula.

purecnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #

Conjunctive normal form (CNF) by essentially the same code. (p. 60)

simpcnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #

cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf Source #

cnf_ :: (IsPropositional pf, Ord pf, JustLiteral lit) => (AtomOf lit -> AtomOf pf) -> Set (Set lit) -> pf Source #

trivial :: (Ord lit, IsLiteral lit) => Set lit -> Bool Source #

Filtering out trivial disjuncts (in this guise, contradictory).

Instance

data Prop Source #

An instance of IsPredicate.

Constructors

 P Fieldspname :: String

Instances

 Source # Methods(==) :: Prop -> Prop -> Bool #(/=) :: Prop -> Prop -> Bool # Source # Methodscompare :: Prop -> Prop -> Ordering #(<) :: Prop -> Prop -> Bool #(<=) :: Prop -> Prop -> Bool #(>) :: Prop -> Prop -> Bool #(>=) :: Prop -> Prop -> Bool #max :: Prop -> Prop -> Prop #min :: Prop -> Prop -> Prop # Source # MethodsshowsPrec :: Int -> Prop -> ShowS #show :: Prop -> String #showList :: [Prop] -> ShowS # Source # Methods Source # MethodspPrint :: Prop -> Doc #pPrintList :: PrettyLevel -> [Prop] -> Doc # Source # Methods Source #

data PFormula atom Source #

An instance of IsPropositional.

Constructors

 F T Atom atom Not (PFormula atom) And (PFormula atom) (PFormula atom) Or (PFormula atom) (PFormula atom) Imp (PFormula atom) (PFormula atom) Iff (PFormula atom) (PFormula atom)

Instances