Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Logic.ATP.Tableaux

Description

Tableaux, seen as an optimized version of a Prawitz-like procedure.

Documentation

prawitz :: forall formula atom term function v. (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int Source #

newtype K Source #

Constructors

Instances details

Enum K Source #
Instance details Defined in Data.Logic.ATP.Tableaux Methods succ :: K -> K # pred :: K -> K # toEnum :: Int -> K # fromEnum :: K -> Int # enumFrom :: K -> [K] # enumFromThen :: K -> K -> [K] # enumFromTo :: K -> K -> [K] # enumFromThenTo :: K -> K -> K -> [K] #
Show K Source #
Instance details Defined in Data.Logic.ATP.Tableaux Methods showsPrec :: Int -> K -> ShowS # show :: K -> String # showList :: [K] -> ShowS #
Eq K Source #
Instance details Defined in Data.Logic.ATP.Tableaux Methods (==) :: K -> K -> Bool # (/=) :: K -> K -> Bool #
Ord K Source #
Instance details Defined in Data.Logic.ATP.Tableaux Methods compare :: K -> K -> Ordering # (<) :: K -> K -> Bool # (<=) :: K -> K -> Bool # (>) :: K -> K -> Bool # (>=) :: K -> K -> Bool # max :: K -> K -> K # min :: K -> K -> K #
Pretty K Source #
Instance details Defined in Data.Logic.ATP.Tableaux Methods pPrintPrec :: PrettyLevel -> Rational -> K -> Doc # pPrint :: K -> Doc # pPrintList :: PrettyLevel -> [K] -> Doc #

tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => Maybe Depth -> formula -> Failing ((K, Map v term), Depth) Source #