Data.Logic.ATP.DefCNF

Definitional CNF.

Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

Documentation

class NumAtom atom where

Methods

ma :: Integer -> atom

ai :: atom -> Integer

Instances

NumAtom Atom

Defined in Data.Logic.ATP.DefCNF

Methods

ma :: Integer -> Atom

ai :: Atom -> Integer

NumAtom (Knows Integer)

Defined in Data.Logic.ATP.DP

Methods

ma :: Integer -> Knows Integer

ai :: Knows Integer -> Integer

defcnfs :: (IsPropositional pf, JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Set (Set (LFormula (AtomOf pf)))

defcnf1 :: forall pf. (IsPropositional pf, JustPropositional pf, NumAtom (AtomOf pf), Ord pf) => pf -> pf

Overall definitional CNF.

defcnf2 :: (IsPropositional pf, JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> pf

Version tweaked to exploit initial structure.

defcnf3 :: forall pf. (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> pf

Version that guarantees 3-CNF.

Instance

data Atom

Constructors

N String Integer

Instances

NumAtom Atom

Defined in Data.Logic.ATP.DefCNF

Methods

ma :: Integer -> Atom

ai :: Atom -> Integer

IsAtom Atom

Defined in Data.Logic.ATP.DefCNF

HasFixity Atom

Defined in Data.Logic.ATP.DefCNF

Methods

precedence :: Atom -> Precedence

associativity :: Atom -> Associativity

Show Atom

Defined in Data.Logic.ATP.DefCNF

Methods

showsPrec :: Int -> Atom -> ShowS

show :: Atom -> String

showList :: [Atom] -> ShowS

Eq Atom

Defined in Data.Logic.ATP.DefCNF

Methods

(==) :: Atom -> Atom -> Bool

(/=) :: Atom -> Atom -> Bool

Ord Atom

Defined in Data.Logic.ATP.DefCNF

Methods

compare :: Atom -> Atom -> Ordering

(<) :: Atom -> Atom -> Bool

(<=) :: Atom -> Atom -> Bool

(>) :: Atom -> Atom -> Bool

(>=) :: Atom -> Atom -> Bool

max :: Atom -> Atom -> Atom

min :: Atom -> Atom -> Atom

Pretty Atom

Defined in Data.Logic.ATP.DefCNF

Methods

pPrintPrec :: PrettyLevel -> Rational -> Atom -> Doc

pPrint :: Atom -> Doc

pPrintList :: PrettyLevel -> [Atom] -> Doc

Tests

testDefCNF :: Test