Data.Logic.ATP.Prop

Propositional formulas

class IsPropositional formula

data BinOp

binop

(⇒)

(==>)

(⊃)

(→)

(⇔)

(<=>)

(↔)

(<==>)

(∧)

·

(∨)

foldPropositional

zipPropositional

convertPropositional

convertToPropositional

precedencePropositional

associativityPropositional

prettyPropositional

showPropositional

onatomsPropositional

overatomsPropositional

Restricted propositional formula class

class JustPropositional formula

Interpretation of formulas.

eval

atoms

Truth Tables

data TruthTable a

onallvaluations

truthTable

Tautologies and related concepts

tautology

unsatisfiable

satisfiable

Substitution

psubst

Dualization

dual

Simplification

psimplify

psimplify1

Normal forms

nnf

nenf

list_conj

list_disj

mk_lits

allsatvaluations

dnfSet

purednf

simpdnf

rawdnf

dnf

purecnf

simpcnf

cnf'

cnf_

trivial

Instance

data Prop

data PFormula atom

Tests

testProp