Data.Logic.ATP.DefCNF

Definitional CNF.

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

Documentation

class NumAtom atom where

Minimal complete definition

ma, ai

Methods

ma :: Integer -> atom

ai :: atom -> Integer

Instances

NumAtom Atom

Methods

ma :: Integer -> Atom

ai :: Atom -> 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

Eq Atom

Methods

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

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

Ord Atom

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

Show Atom

Methods

showsPrec :: Int -> Atom -> ShowS

show :: Atom -> String

showList :: [Atom] -> ShowS

Pretty Atom

Methods

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

pPrint :: Atom -> Doc

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

HasFixity Atom

Methods

precedence :: Atom -> Precedence

associativity :: Atom -> Associativity

IsAtom Atom

NumAtom Atom

Methods

ma :: Integer -> Atom

ai :: Atom -> Integer

Tests

testDefCNF :: Test