Improve documentation

aztek · Jan 6, 2021 · 125476c · 125476c
1 parent 3f8fa44
commit 125476c
Show file tree

Hide file tree

Showing 7 changed files with 133 additions and 62 deletions.
diff --git a/src/ATP.hs b/src/ATP.hs
@@ -5,13  5,30 @@ Copyright    : (c) Evgenii Kotelnikov, 2019
 License      : GPL-3
 Maintainer   : [email protected]
 Stability    : experimental
 
 Express theorems in first-order logic and automatically prove them
 using third-party reasoning tools.
 -}
 
 module ATP (
   -- * First-order logic
   -- $fol
   module ATP.FOL,
 
   -- * Pretty printing for formulas, theorems and proofs
   -- $pretty
   module ATP.Pretty.FOL,
 
   -- * Interface to automated theorem provers
   -- $prove
   module ATP.Prove,
 
   -- * Models of automated theorem provers
   -- $prover
   module ATP.Prover,
 
   -- * Error handling
   -- $error
   module ATP.Error
 ) where
 
@@ -20,3  37,64 @@ import ATP.Pretty.FOL
 import ATP.Prove
 import ATP.Prover
 import ATP.Error
 
 -- $fol
 -- Consider the following classical logical syllogism.
 --
 -- /All humans are mortal. Socrates is a human. Therefore, Socrates is mortal./
 --
 -- We can formalize it in first-order logic as follows.
 --
 -- > human, mortal :: UnaryPredicate
 -- > human = UnaryPredicate "human"
 -- > mortal = UnaryPredicate "mortal"
 -- >
 -- > socrates :: Constant
 -- > socrates = "socrates"
 -- >
 -- > humansAreMortal, socratesIsHuman, socratesIsMortal :: Formula
 -- > humansAreMortal = forall $ \x -> human x ==> mortal x
 -- > socratesIsHuman = human socrates
 -- > socratesIsMortal = mortal socrates
 -- >
 -- > syllogism :: Theorem
 -- > syllogism = [humansAreMortal, socratesIsHuman] |- socratesIsMortal
 
 -- $pretty
 -- 'pprint' pretty-prints theorems and proofs.
 --
 -- >>> pprint syllogism
 -- Axiom 1. ∀ x . (human(x) => mortal(x))
 -- Axiom 2. human(socrates)
 -- Conjecture. mortal(socrates)
 
 -- $prove
 -- 'prove' runs a 'defaultProver' and parses the proof that it produces.
 --
 -- >>> prove syllogism >>= pprint
 -- Found a proof by refutation.
 -- 1. human(socrates) [axiom]
 -- 2. ∀ x . (human(x) => mortal(x)) [axiom]
 -- 3. mortal(socrates) [conjecture]
 -- 4. ￢mortal(socrates) [negated conjecture 3]
 -- 5. ∀ x . (￢human(x) ⋁ mortal(x)) [variable_rename 2]
 -- 6. mortal(x) ⋁ ￢human(x) [split_conjunct 5]
 -- 7. mortal(socrates) [paramodulation 6, 1]
 -- 8. ⟘ [cn 4, 7]
 --
 -- The proof returned by the theorem prover is a directed acyclic graph of
 -- logical inferences. Each logical 'Inference' is a step of the proof that
 -- derives a conclusion from a set of premises using an inference 'Rule'.
 -- The proof ends with a 'Contradiction' and therefore is a proof by
 -- 'Refutation'.
 
 -- $prover
 -- By default 'prove' runs the E theorem prover ('eprover'). Currently,
 -- 'eprover' and 'vampire' are supported.
 --
 -- 'proveUsing' runs a specified theorem prover.
 
 -- $error
 -- A theorem prover might not succeed to construct a proof. Therefore the result
 -- of 'prove' is wrapped in the 'Partial' monad that represents a possible
 -- 'Error', for example 'TimeLimitError' or 'ParsingError'.
diff --git a/src/ATP/Error.hs b/src/ATP/Error.hs
@@ -8,6  8,8 @@ Copyright    : (c) Evgenii Kotelnikov, 2019-2020
 License      : GPL-3
 Maintainer   : [email protected]
 Stability    : experimental
 
 Monads and monad transformers for computations with errors.
 -}
 
 module ATP.Error (

diff --git a/src/ATP/FOL.hs b/src/ATP/FOL.hs
@@ -1,34  1,13 @@
 {-|
 Module       : ATP.FOL
-Description  : Unsorted first-order logic.
 Description  : Syntax of first-order logic.
 Copyright    : (c) Evgenii Kotelnikov, 2019-2020
 License      : GPL-3
 Maintainer   : [email protected]
 Stability    : experimental
 
 Data structures that represent formulas and theorems in first-order logic,
 and smart constructors for them.
-
-Consider the following classical logical syllogism.
-
-/All humans are mortal. Socrates is a human. Therefore, Socrates is mortal./
-
-We can formalize it in first-order logic and express in Haskell as follows.
-
-> human, mortal :: UnaryPredicate
-> human = UnaryPredicate "human"
-> mortal = UnaryPredicate "mortal"
->
-> socrates :: Constant
-> socrates = "socrates"
->
-> humansAreMortal, socratesIsHuman, socratesIsMortal :: Formula
-> humansAreMortal = forall $ \x -> human x ==> mortal x
-> socratesIsHuman = human socrates
-> socratesIsMortal = mortal socrates
->
-> syllogism :: Theorem
-> syllogism = [humansAreMortal, socratesIsHuman] |- socratesIsMortal
 -}
 
 module ATP.FOL (

diff --git a/src/ATP/FirstOrder/Derivation.hs b/src/ATP/FirstOrder/Derivation.hs
@@ -20,7  20,6 @@ module ATP.FirstOrder.Derivation (
   ruleName,
   Inference(..),
   antecedents,
-  consequent,
   Contradiction(..),
   Sequent(..),
   Derivation(..),
@@ -106,24  105,22 @@ ruleName = \case
 --
 -- where each of @A_1@, ... @A_n@ (called the 'antecedents'), and @C@
 -- (called the 'consequent') are formulas and @R@ is an inference 'Rule'.
-data Inference f = Inference (Rule f) LogicalExpression
-  deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 data Inference f = Inference {
   inferenceRule :: Rule f,
   consequent :: LogicalExpression
 } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 
 -- | The antecedents of an inference.
 antecedents :: Inference f -> [f]
-antecedents (Inference rule _) = toList rule
-
--- | The consequent of an inference.
-consequent :: Inference f -> LogicalExpression
-consequent (Inference _ e) = e
 antecedents = toList
 
--- | Contradiction is a special case of an inference whos consequent is
--- a logical falsum.
 -- | Contradiction is a special case of an inference that has the logical falsum
 -- as the consequent.
 newtype Contradiction f = Contradiction (Rule f)
   deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 
 -- | A sequent is a logical inference, annotated with a label.
--- Sequents are chained in 'Derivation's.
 -- Linked sequents form derivations.
 data Sequent f = Sequent f (Inference f)
   deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 
@@ -160,17  157,17 @@ distances (Derivation m) = fmap distance m
       | null (antecedents i) = 0
       | otherwise = 1   maximum (fmap (\a -> distance (m ! a)) (antecedents i))
 
--- | A refutation is a special case of a derivation that results in
--- contradiction. A successful proof produces by an automated theorem prover is
--- a proof by refutation.
 -- | A refutation is a special case of a derivation that results in a
 -- contradiction. A successful proof produces by an automated theorem prover
 -- is a proof by refutation.
 data Refutation f = Refutation (Derivation f) (Contradiction f)
   deriving (Show, Eq, Ord)
 
 -- | The solution produced by an automated first-order theorem prover.
 data Solution
   = Saturation (Derivation Integer)
   -- ^ A theorem can be disproven if the prover constructs a saturated set of
-  -- firt-order clauses.
   -- first-order clauses.
   | Proof (Refutation Integer)
   -- ^ A theorem can be proven if the prover derives contradiction (the empty
   -- clause) from the set of axioms and the negated conjecture.

diff --git a/src/ATP/Pretty/FOL.hs b/src/ATP/Pretty/FOL.hs
@@ -11,6  11,8 @@ Copyright    : (c) Evgenii Kotelnikov, 2019-2020
 License      : GPL-3
 Maintainer   : [email protected]
 Stability    : experimental
 
 Pretty-printers for formulas, theorems and proofs.
 -}
 
 module ATP.Pretty.FOL (

diff --git a/src/ATP/Prove.hs b/src/ATP/Prove.hs
@@ -3,17  3,18 @@
 
 {-|
 Module       : ATP.Prove
-Description  : Interface for calling an automated theorem prover.
 Description  : Interface to automated theorem provers.
 Copyright    : (c) Evgenii Kotelnikov, 2019
 License      : GPL-3
 Maintainer   : [email protected]
 Stability    : experimental
 
 Interface to automated theorem provers.
 -}
 
 module ATP.Prove (
   ProvingOptions(..),
   defaultOptions,
-  defaultProver,
   refute,
   refuteUsing,
   refuteWith,
@@ -42,10  43,10 @@ import ATP.Prover
 -- how to run it.
 data ProvingOptions = ProvingOptions {
   prover      :: Prover,
-  timeLimit   :: Int,    -- ^ The time limit given to the prover, in seconds
-  memoryLimit :: Int,    -- ^ The memory limit given to the prover, in Mb
-  debug       :: Bool    -- ^ If @True@, print the input, the cli command,
-                         --   the exit code and the output of the prover
   timeLimit   :: TimeLimit,
   memoryLimit :: MemoryLimit,
   debug       :: Bool -- ^ If @True@, print the input, the cli command,
                       --   the exit code and the output of the prover
 } deriving (Eq, Show, Ord)
 
 -- | The default options used by 'refute' and 'prove'.
@@ -60,14  61,9 @@ defaultOptions = ProvingOptions {
   debug = False
 }
 
--- | The default prover used by 'refute' and 'prove'.
---
--- >>> defaultProver
--- Prover {vendor = E, executable = "eprover"}
-defaultProver :: Prover
-defaultProver = eprover
-
 -- | Attempt to refute a set of clauses using 'defaultProver'.
 --
 -- > refute = refuteWith defaultOptions
 refute :: Clauses -> IO (Partial Solution)
 refute = refuteWith defaultOptions
 
@@ -80,6  76,8 @@ refuteWith :: ProvingOptions -> Clauses -> IO (Partial Solution)
 refuteWith opts = runWith opts . encodeClauses
 
 -- | Attempt to prove a theorem using 'defaultProver'.
 --
 -- > prove = proveWith defaultOptions
 prove :: Theorem -> IO (Partial Solution)
 prove = proveWith defaultOptions
 
@@ -105,13  103,12 @@ runProver :: ProvingOptions -> String -> IO (ExitCode, Text, Text)
 runProver opts input = do
   let ProvingOptions{prover, timeLimit, memoryLimit, debug} = opts
   let Prover{vendor, executable} = prover
-  let command = proverCommand prover timeLimit memoryLimit
   let arguments = proverArguments vendor timeLimit memoryLimit
   let debugPrint header str = when debug $
                               print (bold (text header)) >>
                               putStrLn str >> putStr "\n"
   debugPrint "Input" input
-  debugPrint "Command" command
   debugPrint "Command" $ unwords (executable:arguments)
   (exitCode, stdout, stderr) <- readProcessWithExitCode executable arguments input
   debugPrint "Exit code" (show exitCode)
   debugPrint "Standard output" stdout

diff --git a/src/ATP/Prover.hs b/src/ATP/Prover.hs
@@ -8,17  8,21 @@ Copyright    : (c) Evgenii Kotelnikov, 2019
 License      : GPL-3
 Maintainer   : [email protected]
 Stability    : experimental
 
 Models of automated theorem provers.
 -}
 
 module ATP.Prover (
   Vendor(..),
   Prover(..),
-  proverCommand,
   TimeLimit,
   MemoryLimit,
   proverArguments,
   proverOutput,
   vampire,
   eprover,
-  cvc4
   cvc4,
   defaultProver
 ) where
 
 import Data.Text (Text)
@@ -41,13  45,14 @@ data Vendor
   | CVC4
   deriving (Eq, Show, Ord, Enum, Bounded)
 
--- | Build the command that executes the given prover.
-proverCommand :: Prover -> Int -> Int -> String
-proverCommand Prover{vendor, executable} timeLimit memoryLimit =
-  unwords (executable:proverArguments vendor timeLimit memoryLimit)
 -- | The time limit allocated to the prover, in seconds.
 type TimeLimit = Int
 
 -- | The memory limit allocated to the prover, in Mb.
 type MemoryLimit = Int
 
 -- | Build the list of command line arguments for the given prover.
-proverArguments :: Vendor -> Int -> Int -> [String]
 proverArguments :: Vendor -> TimeLimit -> MemoryLimit -> [String]
 proverArguments E timeLimit memoryLimit =
   ["--proof-object",
    "--silent",
@@ -60,12  65,16 @@ proverArguments Vampire timeLimit memoryLimit =
    "--memory_limit", show memoryLimit]
 proverArguments CVC4 timeLimit _memoryLimit =
   ["-L", "tptp",
-   "--proof", "--output-lang=tptp",
    "--proof", "--dump-proof", "--output-lang=tptp",
    "--tlimit="    show (timeLimit * 1000)]
 
 -- | Interpret the output of the theorem prover from its exit code and
 -- the contents of the returned stdout and stderr.
-proverOutput :: Vendor -> ExitCode -> Text -> Text -> Partial Text
 proverOutput :: Vendor
              -> ExitCode
              -> Text -- ^ Standard out
              -> Text -- ^ Standard error
              -> Partial Text
 proverOutput E exitCode stdout stderr = case exitCode of
   ExitSuccess   -> return stdout
   ExitFailure 1 -> return stdout
@@ -99,4  108,11 @@ cvc4 :: Prover
 cvc4 = Prover {
   vendor = CVC4,
   executable = "cvc4"
-}
 }
 
 -- | The default prover used by @refute@ and @prove@.
 --
 -- >>> defaultProver
 -- Prover {vendor = E, executable = "eprover"}
 defaultProver :: Prover
 defaultProver = eprover