atp-haskell-1.10: Translation from Ocaml to Haskell of John Harrison's ATP code

Safe HaskellNone
LanguageHaskell98

Data.Logic.ATP.DefCNF

Contents

Description

Definitional CNF.

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

Synopsis

Documentation

class NumAtom atom where Source

Methods

ma :: Integer -> atom Source

ai :: atom -> Integer Source

Instances

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

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

Overall definitional CNF.

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

Version tweaked to exploit initial structure.

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

Version that guarantees 3-CNF.

Instance

data Atom Source

Constructors

N String Integer 

Instances

Tests

testDefCNF :: Test Source