Running the theorem prover eprover in parallel:
import Prelude hiding (mapM)
import Data.Traversable
import Data.List
import Data.Maybe
import Control.Concurrent.STM.Promise
import Control.Concurrent.STM.Promise.Process
import Control.Concurrent.STM.Promise.Tree
import Control.Concurrent.STM.Promise.Workers
{- | A tree for this file structure:
├── mul-commutative
│ ├── induction_x_0.tptp
│ ├── induction_x_1.tptp
│ ├── induction_x_y_0.tptp
│ ├── induction_x_y_1.tptp
│ ├── induction_x_y_2.tptp
│ ├── induction_x_y_3.tptp
│ ├── induction_y_0.tptp
│ ├── induction_y_1.tptp
│ └── no_induction_0.tptp
└── plus-commutative
├── induction_x_0.tptp
├── induction_x_1.tptp
├── induction_x_y_0.tptp
├── induction_x_y_1.tptp
├── induction_x_y_2.tptp
├── induction_x_y_3.tptp
├── induction_y_0.tptp
├── induction_y_1.tptp
└── no_induction_0.tptp
-}
file_tree :: Tree FilePath
file_tree = fmap (++ ".tptp") $ tryAll
[ fmap ("mul-commutative/" ++) $ requireAny
[ fmap ("induction_x_" ++) $ requireAll $ map Leaf ["0","1"]
, fmap ("induction_y_" ++) $ requireAll $ map Leaf ["0","1"]
, fmap ("induction_x_y_" ++) $ requireAll $ map Leaf ["0","1","2","3"]
, Leaf "no_induction_0"
]
, fmap ("plus-commutative/" ++) $ requireAny
[ fmap ("induction_x_" ++) $ requireAll $ map Leaf ["0","1"]
, fmap ("induction_y_" ++) $ requireAll $ map Leaf ["0","1"]
, fmap ("induction_x_y_" ++) $ requireAll $ map Leaf ["0","1","2","3"]
, Leaf "no_induction_0"
]
]
success :: ProcessResult -> Bool
success r = excode r == ExitSuccess && any (`isInfixOf` stdout r) ok
where
ok = ["Theorem","Unsatisfiable"]
eproverPromise :: FilePath -> IO (Promise [(FilePath,Bool)])
eproverPromise file = do
let args = ["-xAuto","-tAuto",'-':"-tptp3-format","-s"]
promise <- processPromise "eprover" (file : args) ""
let chres :: ProcessResult -> [(FilePath,Bool)]
chres r = [ (file,success r) ]
return $ fmap chres promise
main :: IO ()
main = do
promise_tree <- mapM eproverPromise file_tree
let timeout = 1000 * 1000 -- microseconds
processes = 2
workers (Just timeout) processes (interleave promise_tree)
res <- evalTree (any (not . snd)) promise_tree
putStrLn "Results: "
mapM_ print res
The result of this run is:
Results:
("plus-commutative/induction_x_y_0.tptp",True)
("plus-commutative/induction_x_y_1.tptp",True)
("plus-commutative/induction_x_y_2.tptp",True)
("plus-commutative/induction_x_y_3.tptp",True)
This means that four out of four obligations for commutativity of plus succeeded when doing induction on both x and y.