diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -11,10 +11,7 @@ cabal install twee -fllvm If you really want the latest unstable version, run -`cabal install src/ .` in this repository. You will most likely need -the latest git version of Jukebox, from -https://github.com/nick8325/jukebox, too - and things may break from -time to time. +`cabal install src/ .` in this repository. Afterwards, run `twee nameofproblem.p`. The problem should be in TPTP format (http://www.tptp.org). You can find a few examples in the diff --git a/executable/Main.hs b/executable/Main.hs --- a/executable/Main.hs +++ b/executable/Main.hs @@ -1,692 +1,1 @@ -{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards #-} -{-# OPTIONS_GHC -flate-specialise #-} -import Control.Monad -import Data.Char -import Data.Either -import Twee hiding (message) -import Twee.Base hiding (char, lookup, vars) -import Twee.Rule(lhs, rhs, unorient) -import Twee.Equation -import qualified Twee.Proof as Proof -import Twee.Proof hiding (Config, defaultConfig) -import qualified Twee.Join as Join -import Twee.Utils -import qualified Twee.CP as CP -import Data.Ord -import qualified Data.Map.Strict as Map -import qualified Twee.KBO as KBO -import Data.List.Split -import Data.List -import Data.Maybe -import Jukebox.Options -import Jukebox.Toolbox -import Jukebox.Name hiding (lhs, rhs, label) -import qualified Jukebox.Form as Jukebox -import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size, matchList) -import Jukebox.Tools.EncodeTypes -import Jukebox.TPTP.Print -import Jukebox.Tools.HornToUnit -import qualified Data.IntMap.Strict as IntMap -import System.IO -import System.Exit -import qualified Data.Set as Set -import Twee.Label - -data MainFlags = - MainFlags { - flags_proof :: Bool, - flags_trace :: Maybe (String, String), - flags_casc :: Bool, - flags_explain_encoding :: Bool } - -parseMainFlags :: OptionParser MainFlags -parseMainFlags = - MainFlags <$> proof <*> trace <*> casc <*> explain - where - proof = - inGroup "Output options" $ - bool "proof" ["Produce proofs (on by default)."] - True - trace = - expert $ - inGroup "Output options" $ - flag "trace" - ["Write a Prolog-format execution trace to this file (off by default)."] - Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule) - casc = - expert $ - inGroup "Output options" $ - bool "casc" ["Print output in CASC format (off by default)."] False - explain = - expert $ - inGroup "Output options" $ - bool "explain-encoding" ["In CASC mode, explain the conditional encoding (off by default)."] False - - argModule = arg "" "expected a Prolog module name" Just - -parseConfig :: OptionParser (Config (Extended Constant)) -parseConfig = - Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> simplify <*> normPercent <*> - (CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor) <*> - (Join.Config <$> ground_join <*> connectedness <*> set_join) <*> - (Proof.Config <$> all_lemmas <*> flat_proof <*> show_instances) - where - maxSize = - inGroup "Resource limits" $ - flag "max-term-size" ["Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default)."] Nothing (Just <$> checkSize <$> argNum) - checkSize n t = size t <= n - maxCPs = - inGroup "Resource limits" $ - flag "max-cps" ["Give up after considering this many critical pairs (unlimited by default)."] maxBound argNum - maxCPDepth = - inGroup "Resource limits" $ - flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum - simplify = - expert $ - inGroup "Completion heuristics" $ - bool "simplify" - ["Simplify rewrite rules with respect to one another (on by default)."] - True - normPercent = - expert $ - inGroup "Completion heuristics" $ - defaultFlag "normalise-queue-percent" "Percent of time spent renormalising queued critical pairs" (cfg_renormalise_percent) argNum - lweight = - expert $ - inGroup "Critical pair weighting heuristics" $ - defaultFlag "lhs-weight" "Weight given to LHS of critical pair" (CP.cfg_lhsweight . cfg_critical_pairs) argNum - rweight = - expert $ - inGroup "Critical pair weighting heuristics" $ - defaultFlag "rhs-weight" "Weight given to RHS of critical pair" (CP.cfg_rhsweight . cfg_critical_pairs) argNum - funweight = - expert $ - inGroup "Critical pair weighting heuristics" $ - defaultFlag "fun-weight" "Weight given to function symbols" (CP.cfg_funweight . cfg_critical_pairs) argNum - varweight = - expert $ - inGroup "Critical pair weighting heuristics" $ - defaultFlag "var-weight" "Weight given to variable symbols" (CP.cfg_varweight . cfg_critical_pairs) argNum - depthweight = - expert $ - inGroup "Critical pair weighting heuristics" $ - defaultFlag "depth-weight" "Weight given to critical pair depth" (CP.cfg_depthweight . cfg_critical_pairs) argNum - dupcost = - expert $ - inGroup "Critical pair weighting heuristics" $ - defaultFlag "dup-cost" "Cost of duplicate subterms" (CP.cfg_dupcost . cfg_critical_pairs) argNum - dupfactor = - expert $ - inGroup "Critical pair weighting heuristics" $ - defaultFlag "dup-factor" "Size factor of duplicate subterms" (CP.cfg_dupfactor . cfg_critical_pairs) argNum - ground_join = - expert $ - inGroup "Critical pair joining heuristics" $ - bool "ground-joining" - ["Test terms for ground joinability (on by default)."] - True - connectedness = - expert $ - inGroup "Critical pair joining heuristics" $ - bool "connectedness" - ["Test terms for subconnectedness (on by default)."] - True - set_join = - expert $ - inGroup "Critical pair joining heuristics" $ - bool "set-join" - ["Compute all normal forms when joining critical pairs (off by default)."] - False - all_lemmas = - expert $ - inGroup "Proof presentation" $ - bool "all-lemmas" - ["Produce a proof with one lemma for each critical pair (off by default)."] - False - flat_proof = - expert $ - inGroup "Proof presentation" $ - bool "no-lemmas" - ["Produce a proof with no lemmas (off by default).", - "May lead to exponentially large proofs."] - False - show_instances = - expert $ - inGroup "Proof presentation" $ - bool "show-instances" - ["Show which instances of each axiom and lemma were used (off by default)."] - False - defaultFlag name desc field parser = - flag name [desc ++ " (" ++ show def ++ " by default)."] def parser - where - def = field defaultConfig - -parsePrecedence :: OptionParser [String] -parsePrecedence = - expert $ - inGroup "Term order options" $ - fmap (splitOn ",") - (flag "precedence" ["List of functions in descending order of precedence."] [] (arg "" "expected a function name" Just)) - -data Constant = - Constant { - con_prec :: {-# UNPACK #-} !Precedence, - con_id :: {-# UNPACK #-} !Jukebox.Function, - con_arity :: {-# UNPACK #-} !Int, - con_size :: {-# UNPACK #-} !Int, - con_bonus :: !Bool } - deriving (Eq, Ord) - -data Precedence = Precedence !Bool !Bool !(Maybe Int) !Int - deriving (Eq, Ord) - -instance Sized Constant where - size Constant{..} = con_size -instance Arity Constant where - arity Constant{..} = con_arity - -instance Pretty Constant where - pPrint Constant{..} = text (base con_id) - -instance PrettyTerm Constant where - termStyle Constant{..} - | hasLabel "type_tag" con_id = invisible - | any isAlphaNum (base con_id) = uncurried - | otherwise = - case con_arity of - 1 -> prefix - 2 -> infixStyle 5 - _ -> uncurried - -instance Ordered (Extended Constant) where - lessEq t u = {-# SCC lessEq #-} KBO.lessEq t u - lessIn model t u = {-# SCC lessIn #-} KBO.lessIn model t u - -instance EqualsBonus Constant where - hasEqualsBonus = con_bonus - isEquals = Main.isEquals . con_id - isTrue = Main.isTrue . con_id - isFalse = Main.isFalse . con_id - -data TweeContext = - TweeContext { - ctx_var :: Jukebox.Variable, - ctx_minimal :: Jukebox.Function, - ctx_true :: Jukebox.Function, - ctx_false :: Jukebox.Function, - ctx_equals :: Jukebox.Function, - ctx_type :: Type } - --- Convert back and forth between Twee and Jukebox. -tweeConstant :: HornFlags -> TweeContext -> Precedence -> Jukebox.Function -> Extended Constant -tweeConstant flags TweeContext{..} prec fun - | fun == ctx_minimal = Minimal - | otherwise = Function (Constant prec fun (Jukebox.arity fun) (sz fun) (bonus fun)) - where - sz fun = if isType fun then 0 else 1 - bonus fun = - (isIfeq fun && encoding flags /= Asymmetric2) || - Main.isEquals fun - -isType :: Jukebox.Function -> Bool -isType fun = - hasLabel "type_tag" (name fun) && Jukebox.arity fun == 1 - -isIfeq :: Jukebox.Function -> Bool -isIfeq fun = - hasLabel "ifeq" (name fun) - -isEquals :: Jukebox.Function -> Bool -isEquals fun = - hasLabel "equals" (name fun) && Jukebox.arity fun == 2 - -isTrue :: Jukebox.Function -> Bool -isTrue fun = - hasLabel "true" (name fun) && Jukebox.arity fun == 0 - -isFalse :: Jukebox.Function -> Bool -isFalse fun = - hasLabel "false" (name fun) && Jukebox.arity fun == 0 - -jukeboxFunction :: TweeContext -> Extended Constant -> Jukebox.Function -jukeboxFunction _ (Function Constant{..}) = con_id -jukeboxFunction TweeContext{..} Minimal = ctx_minimal -jukeboxFunction TweeContext{..} (Skolem _) = - error "Skolem variable leaked into rule" - -tweeTerm :: HornFlags -> TweeContext -> (Jukebox.Function -> Precedence) -> Jukebox.Term -> Term (Extended Constant) -tweeTerm flags ctx prec t = build (tm t) - where - tm (Jukebox.Var (x ::: _)) = - var (V (fromIntegral (labelNum (label x)))) - tm (f :@: ts) = - app (fun (tweeConstant flags ctx (prec f) f)) (map tm ts) - -jukeboxTerm :: TweeContext -> Term (Extended Constant) -> Jukebox.Term -jukeboxTerm TweeContext{..} (Var (V x)) = - Jukebox.Var (Unique (fromIntegral x) "X" Nothing defaultRenamer ::: ctx_type) -jukeboxTerm ctx@TweeContext{..} (App f t) = - jukeboxFunction ctx (fun_value f) :@: map (jukeboxTerm ctx) ts - where - ts = unpack t - -makeContext :: Problem Clause -> TweeContext -makeContext prob = run prob $ \prob -> do - let - ty = - case types' prob of - [] -> indType - [ty] -> ty - - var <- newSymbol "X" ty - minimal <- newFunction (withLabel "minimal" (name "constant")) [] ty - true <- newFunction (withLabel "true" (name "true")) [] ty - false <- newFunction (withLabel "false" (name "false")) [] ty - equals <- newFunction (withLabel "equals" (name "equals")) [ty, ty] ty - - return TweeContext { - ctx_var = var, - ctx_minimal = minimal, - ctx_true = true, - ctx_false = false, - ctx_equals = equals, - ctx_type = ty } - --- Encode existentials so that all goals are ground. -addNarrowing :: TweeContext -> Problem Clause -> Problem Clause -addNarrowing TweeContext{..} prob = - unchanged ++ equalityClauses - where - (unchanged, nonGroundGoals) = partitionEithers (map f prob) - where - f inp@Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])} - | not (ground x) || not (ground y) = - Right (inp, (x, y)) - f inp = Left inp - - equalityClauses - | null nonGroundGoals = [] - | otherwise = - -- Turn a != b & c != d & ... - -- into eq(a,b)=false & eq(c,d)=false & eq(X,X)=true & true!=false (esa) - -- and then extract the individual components (thm) - let - equalityLiterals = - -- true != false - ("true_equals_false", Neg ((ctx_true :@:) [] Jukebox.:=: (ctx_false :@: []))): - -- eq(X,X)=true - ("reflexivity", Pos (ctx_equals :@: [Jukebox.Var ctx_var, Jukebox.Var ctx_var] Jukebox.:=: (ctx_true :@: []))): - -- [eq(a,b)=false, eq(c,d)=false, ...] - [ (tag, Pos (ctx_equals :@: [x, y] Jukebox.:=: (ctx_false :@: []))) - | (Input{tag = tag}, (x, y)) <- nonGroundGoals ] - - -- Equisatisfiable to the input clauses - justification = - Input { - tag = "new_negated_conjecture", - kind = Jukebox.Ax NegatedConjecture, - what = - let form = And (map (Literal . snd) equalityLiterals) in - ForAll (Bind (Set.fromList (vars form)) form), - source = - Inference "encode_existential" "esa" - (map (fmap toForm . fst) nonGroundGoals) } - - input tag form = - Input { - tag = tag, - kind = Conj Conjecture, - what = clause [form], - source = - Inference "split_conjunct" "thm" [justification] } - - in [input tag form | (tag, form) <- equalityLiterals] - -data PreEquation = - PreEquation { - pre_name :: String, - pre_form :: Input Form, - pre_eqn :: (Jukebox.Term, Jukebox.Term) } - --- Split the problem into axioms and ground goals. -identifyProblem :: - TweeContext -> Problem Clause -> Either (Input Clause) ([PreEquation], [PreEquation]) -identifyProblem TweeContext{..} prob = - fmap partitionEithers (mapM identify prob) - - where - pre inp x = - PreEquation { - pre_name = tag inp, - pre_form = fmap toForm inp, - pre_eqn = x } - - identify inp@Input{what = Clause (Bind _ [Pos (t Jukebox.:=: u)])} = - return $ Left (pre inp (t, u)) - identify inp@Input{what = Clause (Bind _ [Neg (t Jukebox.:=: u)])} - | ground t && ground u = - return $ Right (pre inp (t, u)) - identify inp@Input{what = Clause (Bind _ [])} = - -- The empty clause can appear after clausification if - -- the conjecture was trivial - return $ Left (pre inp (Jukebox.Var ctx_var, ctx_minimal :@: [])) - identify inp = Left inp - -runTwee :: GlobalFlags -> TSTPFlags -> MainFlags -> HornFlags -> Config (Extended Constant) -> [String] -> (IO () -> IO ()) -> Problem Clause -> IO Answer -runTwee globals (TSTPFlags tstp) main horn config precedence later obligs = {-# SCC runTwee #-} do - let - -- Encode whatever needs encoding in the problem - ctx = makeContext obligs - prob = prettyNames (addNarrowing ctx obligs) - - (axioms0, goals0) <- - case identifyProblem ctx prob of - Left inp -> do - mapM_ (hPutStrLn stderr) [ - "The problem contains the following clause, which is not a unit equality:", - indent (show (pPrintClauses [inp])), - "Twee only handles unit equality problems."] - exitWith (ExitFailure 1) - Right x -> return x - - let - -- Work out a precedence for function symbols - prec c = - Precedence - (isType c) - (isNothing (elemIndex (base c) precedence)) - (fmap negate (elemIndex (base c) precedence)) - (negate (Map.findWithDefault 0 c occs)) - occs = funsOcc prob - - -- Translate everything to Twee. - toEquation (t, u) = - canonicalise (tweeTerm horn ctx prec t :=: tweeTerm horn ctx prec u) - - goals = - [ goal n pre_name (toEquation pre_eqn) - | (n, PreEquation{..}) <- zip [1..] goals0 ] - axioms = - [ Axiom n pre_name (toEquation pre_eqn) - | (n, PreEquation{..}) <- zip [1..] axioms0 ] - - withGoals = foldl' (addGoal config) initialState goals - withAxioms = foldl' (addAxiom config) withGoals axioms - - -- Set up tracing. - sayTrace <- - case flags_trace main of - Nothing -> return $ \_ -> return () - Just (file, mod) -> do - h <- openFile file WriteMode - hSetBuffering h LineBuffering - let put msg = hPutStrLn h msg - put $ ":- module(" ++ mod ++ ", [step/1, lemma/1])." - put ":- discontiguous(step/1)." - put ":- discontiguous(lemma/1)." - put ":- style_check(-singleton)." - return $ \msg -> hPutStrLn h msg - - let - say msg = unless (quiet globals) (putStrLn msg) - line = say "" - output = Output { - output_message = \msg -> do - say (prettyShow msg) - sayTrace (show (traceMsg msg)) } - - traceMsg (NewActive active) = - step "add" [traceActive active] - traceMsg (NewEquation eqn) = - step "hard" [traceEqn eqn] - traceMsg (DeleteActive active) = - step "delete" [traceActive active] - traceMsg SimplifyQueue = - step "simplify_queue" [] - traceMsg Interreduce = - step "interreduce" [] - - traceActive Active{..} = - traceApp "rule" [pPrint active_id, traceEqn (unorient active_rule)] - traceEqn (t :=: u) = - pPrintPrec prettyNormal 6 t <+> text "=" <+> pPrintPrec prettyNormal 6 u - traceApp f xs = - pPrintTerm uncurried prettyNormal 0 (text f) xs - - step :: String -> [Doc] -> Doc - step f xs = traceApp "step" [traceApp f xs] <#> text "." - - say "Here is the input problem:" - forM_ axioms $ \Axiom{..} -> - say $ show $ nest 2 $ - describeEquation "Axiom" - (show axiom_number) (Just axiom_name) axiom_eqn - forM_ goals $ \Goal{..} -> - say $ show $ nest 2 $ - describeEquation "Goal" - (show goal_number) (Just goal_name) goal_eqn - line - - state <- complete output config withAxioms - line - - when (solved state && flags_proof main) $ later $ do - let - pres = present (cfg_proof_presentation config) (solutions state) - - sayTrace "" - forM_ (pres_lemmas pres) $ \p -> - sayTrace $ show $ - traceApp "lemma" [traceEqn (equation p)] <#> text "." - - when (flags_casc main) $ do - putStrLn "% SZS output start Proof" - let - axiomForms = - Map.fromList - (zip (map axiom_number axioms) (map pre_form axioms0)) - goalForms = - Map.fromList - (zip (map goal_number goals) (map pre_form goals0)) - - findSource forms n = - case Map.lookup n forms of - Nothing -> [] - Just inp -> go inp - where - go Input{source = Unknown} = [] - go Input{source = Inference _ _ inps} = concatMap go inps - go inp@Input{source = FromFile _ _} = [inp] - - when (flags_explain_encoding main) $ do - putStrLn "Take the following subset of the input axioms:" - mapM_ putStrLn $ map (" " ++) $ lines $ showProblem $ - usortBy (comparing show) $ - (pres_axioms pres >>= findSource axiomForms . axiom_number) ++ - (pres_goals pres >>= findSource goalForms . pg_number) - - putStrLn "" - putStrLn "Now clausify the problem and encode Horn clauses using encoding 3 of" - putStrLn "http://www.cse.chalmers.se/~nicsma/papers/horn.pdf." - putStrLn "We repeatedly replace C & s=t => u=v by the two clauses:" - putStrLn " fresh(y, y, x1...xn) = u" - putStrLn " C => fresh(s, t, x1...xn) = v" - putStrLn "where fresh is a fresh function symbol and x1..xn are the free" - putStrLn "variables of u and v." - putStrLn "A predicate p(X) is encoded as p(X)=true (this is sound, because the" - putStrLn "input problem has no model of domain size 1)." - putStrLn "" - putStrLn "The encoding turns the above axioms into the following unit equations and goals:" - putStrLn "" - print $ pPrintPresentation (cfg_proof_presentation config) pres - putStrLn "% SZS output end Proof" - putStrLn "" - - when (tstp && not (flags_casc main)) $ do - putStrLn "% SZS output start CNFRefutation" - print $ pPrintProof $ - presentToJukebox ctx (curry toEquation) - (zip (map axiom_number axioms) (map pre_form axioms0)) - (zip (map goal_number goals) (map pre_form goals0)) - pres - putStrLn "% SZS output end CNFRefutation" - putStrLn "" - - when (not (flags_casc main)) $ do - putStrLn "The conjecture is true! Here is a proof." - putStrLn "" - print $ pPrintPresentation (cfg_proof_presentation config) pres - putStrLn "" - - when (not (quiet globals) && not (solved state)) $ later $ do - let - state' = interreduce config state - score rule = - (size (lhs rule), lhs rule, - size (rhs rule), rhs rule) - actives = - sortBy (comparing (score . active_rule)) $ - IntMap.elems (st_active_ids state') - - when (tstp && configIsComplete config) $ do - putStrLn "% SZS output start Saturation" - print $ pPrintProof $ - map pre_form axioms0 ++ - map pre_form goals0 ++ - [ Input "rule" (Jukebox.Ax Jukebox.Axiom) Unknown $ - toForm $ clause - [Pos (jukeboxTerm ctx (lhs rule) Jukebox.:=: jukeboxTerm ctx (rhs rule))] - | rule <- rules state ] - putStrLn "% SZS output end Saturation" - putStrLn "" - - if configIsComplete config then do - putStrLn "Ran out of critical pairs. This means the conjecture is not true." - else do - putStrLn "Gave up on reaching the given resource limit." - putStrLn "Here is the final rewrite system:" - forM_ actives $ \active -> - putStrLn (" " ++ prettyShow (canonicalise (active_rule active))) - putStrLn "" - - return $ - if solved state then Unsat Unsatisfiable Nothing - else if configIsComplete config && not (dropNonHorn horn) then Sat Satisfiable Nothing - else NoAnswer GaveUp - --- Transform a proof presentation into a Jukebox proof. -presentToJukebox :: - TweeContext -> - (Jukebox.Term -> Jukebox.Term -> Equation (Extended Constant)) -> - -- Axioms, indexed by axiom number. - [(Int, Input Form)] -> - -- N.B. the formula here proves the negated goal. - [(Int, Input Form)] -> - Presentation (Extended Constant) -> - Problem Form -presentToJukebox ctx toEquation axioms goals Presentation{..} = - [ Input { - tag = pg_name, - kind = Jukebox.Ax Jukebox.Axiom, - what = false, - source = - Inference "resolution" "thm" - [-- A proof of t != u - existentialHack pg_goal_hint (fromJust (lookup pg_number goals)), - -- A proof of t = u - fromJust (Map.lookup pg_number goal_proofs)] } - | ProvedGoal{..} <- pres_goals ] - - where - axiom_proofs = - Map.fromList - [ (axiom_number, fromJust (lookup axiom_number axioms)) - | Axiom{..} <- pres_axioms ] - - lemma_proofs = - Map.fromList [(p, tstp p) | p <- pres_lemmas] - - goal_proofs = - Map.fromList [(pg_number, tstp pg_proof) | ProvedGoal{..} <- pres_goals] - - tstp :: Proof (Extended Constant) -> Input Form - tstp = deriv . derivation - - deriv :: Derivation (Extended Constant) -> Input Form - deriv p@(Trans q r) = derivFrom (deriv r:sources q) p - deriv p = derivFrom (sources p) p - - derivFrom :: [Input Form] -> Derivation (Extended Constant) -> Input Form - derivFrom sources p = - Input { - tag = "step", - kind = Jukebox.Ax Jukebox.Axiom, - what = jukeboxEquation (equation (certify p)), - source = - Inference "rw" "thm" sources } - - jukeboxEquation :: Equation (Extended Constant) -> Form - jukeboxEquation (t :=: u) = - toForm $ clause [Pos (jukeboxTerm ctx t Jukebox.:=: jukeboxTerm ctx u)] - - sources :: Derivation (Extended Constant) -> [Input Form] - sources p = - [ fromJust (Map.lookup lemma lemma_proofs) - | lemma <- usort (usedLemmas p) ] ++ - [ fromJust (Map.lookup axiom_number axiom_proofs) - | Axiom{..} <- usort (usedAxioms p) ] - - -- An ugly hack: since Twee.Proof decodes $true = $false into a - -- proof of the existentially quantified goal, we need to do the - -- same decoding at the Jukebox level. - existentialHack eqn input = - case find input of - [] -> error $ "bug in TSTP output: can't fix up decoded existential" - (inp:_) -> inp - where - -- Check if this looks like the correct clause; - -- if not, try its ancestors. - find inp | ok inp = [inp] - find Input{source = Inference _ _ inps} = - concatMap find inps - find _ = [] - - ok inp = - case toClause (what inp) of - Nothing -> False - Just (Clause (Bind _ [Neg (t' Jukebox.:=: u')])) -> - let - eqn' = toEquation t' u' - ts = buildList [eqn_lhs eqn, eqn_rhs eqn] - us = buildList [eqn_lhs eqn', eqn_rhs eqn'] - in - isJust (matchList ts us) && isJust (matchList us ts) - -main = do - hSetBuffering stdout LineBuffering - join . parseCommandLineWithExtraArgs - ["--no-conjunctive-conjectures", "--no-split"] -#ifdef VERSION_twee - "Twee, an equational theorem prover" . version ("twee version " ++ VERSION_twee) $ -#else - "Twee, an equational theorem prover" . version "twee development version" $ -#endif - globalFlags *> parseMainFlags *> - -- hack: get --quiet and --no-proof options to appear before --tstp - forAllFilesBox <*> - (readProblemBox =>>= - expert clausifyBox =>>= - forAllConjecturesBox <*> - (combine <$> - expert hornToUnitBox <*> - (toFormulasBox =>>= - expert (toFof <$> clausifyBox <*> pure (tags True)) =>>= - expert clausifyBox =>>= expert oneConjectureBox) <*> - (runTwee <$> globalFlags <*> tstpFlags <*> parseMainFlags <*> expert hornFlags <*> parseConfig <*> parsePrecedence))) - where - combine horn encode prove later prob = do - res <- horn prob - case res of - Left ans -> return ans - Right prob -> - encode prob >>= prove later +import SequentialMain diff --git a/executable/SequentialMain.hs b/executable/SequentialMain.hs new file mode 100644 --- /dev/null +++ b/executable/SequentialMain.hs @@ -0,0 +1,914 @@ +{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards #-} +{-# OPTIONS_GHC -flate-specialise #-} +module SequentialMain(main) where + +import Control.Monad +import Data.Char +import Data.Either +import Twee hiding (message) +import Twee.Base hiding (char, lookup, vars, ground) +import Twee.Rule(lhs, rhs, unorient) +import Twee.Equation +import qualified Twee.Proof as Proof +import Twee.Proof hiding (Config, defaultConfig) +import qualified Twee.Join as Join +import Twee.Utils +import qualified Twee.CP as CP +import Data.Ord +import qualified Data.Map.Strict as Map +import qualified Twee.KBO as KBO +import Data.List.Split +import Data.List +import Data.Maybe +import Jukebox.Options +import Jukebox.Toolbox +import Jukebox.Name hiding (lhs, rhs, label) +import qualified Jukebox.Form as Jukebox +import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size) +import Jukebox.Tools.EncodeTypes +import Jukebox.TPTP.Print +import Jukebox.Tools.HornToUnit +import qualified Data.IntMap.Strict as IntMap +import System.IO +import System.Exit +import qualified Data.Set as Set +import qualified Twee.Label as Label +import System.Console.ANSI +import Data.Symbol + +data MainFlags = + MainFlags { + flags_proof :: Bool, + flags_trace :: Maybe (String, String), + flags_formal_proof :: Bool, + flags_explain_encoding :: Bool, + flags_flip_ordering :: Bool, + flags_give_up_on_saturation :: Bool, + flags_flatten_goals :: Bool, + flags_flatten_goals_lightly :: Bool, + flags_flatten_all :: Bool, + flags_eliminate :: [String], + flags_backwards_goal :: Int } + +parseMainFlags :: OptionParser MainFlags +parseMainFlags = + MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenLightly <*> flattenAll <*> eliminate <*> backwardsGoal + where + proof = + inGroup "Output options" $ + bool "proof" ["Produce proofs (on by default)."] + True + trace = + expert $ + inGroup "Output options" $ + flag "trace" + ["Write a Prolog-format execution trace to this file (off by default)."] + Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule) + formal = + expert $ + inGroup "Output options" $ + bool "formal-proof" ["Print proof as formal TSTP derivation (requires --tstp; off by default)."] False + explain = + expert $ + inGroup "Output options" $ + bool "explain-encoding" ["In CASC mode, explain the conditional encoding (off by default)."] False + flipOrdering = + expert $ + inGroup "Term order options" $ + bool "flip-ordering" ["Make more common function symbols smaller (off by default)."] False + giveUp = + expert $ + inGroup "Output options" $ + bool "give-up-on-saturation" ["Report SZS status GiveUp rather than Unsatisfiable on saturation (off by default)."] False + flatten = + expert $ + inGroup "Completion heuristics" $ + bool "flatten-goal" ["Flatten goal by adding new axioms (on by default)."] True + flattenLightly = + expert $ + inGroup "Completion heuristics" $ + bool "flatten-goal-lightly" ["Flatten goal non-recursively by adding new axioms (off by default)."] False + flattenAll = + expert $ + inGroup "Completion heuristics" $ + bool "flatten" ["Flatten all clauses by adding new axioms (off by default)."] False + backwardsGoal = + expert $ + inGroup "Completion heuristics" $ + flag "backwards-goal" ["Try rewriting backwards from the goal this many times (0 by default)."] 0 argNum + eliminate = + inGroup "Proof presentation" $ + concat <$> + manyFlags "eliminate" + ["Treat these axioms as definitions and eliminate them from the proof.", + "The axiom must have the shape f(x1...xn) = t, where x1...xn are", + "distinct variables. The term f must not otherwise appear in the problem!", + "This is not checked."] + (splitOn "," <$> arg "" "expected a list of axiom names" Just) + + argModule = arg "" "expected a Prolog module name" Just + +parseConfig :: OptionParser (Config Constant) +parseConfig = + Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> simplify <*> normPercent <*> cpSampleSize <*> cpRenormaliseThreshold <*> set_join_goals <*> always_simplify <*> complete_subsets <*> + (CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor) <*> + (Join.Config <$> ground_join <*> connectedness <*> ground_connectedness <*> set_join) <*> + (Proof.Config <$> all_lemmas <*> flat_proof <*> ground_proof <*> show_instances <*> colour <*> show_axiom_uses) + where + maxSize = + inGroup "Resource limits" $ + flag "max-term-size" ["Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default)."] Nothing (Just <$> checkSize <$> argNum) + checkSize n t = KBO.size t <= n + maxCPs = + inGroup "Resource limits" $ + flag "max-cps" ["Give up after considering this many critical pairs (unlimited by default)."] maxBound argNum + maxCPDepth = + inGroup "Resource limits" $ + flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum + simplify = + expert $ + inGroup "Completion heuristics" $ + bool "simplify" + ["Simplify rewrite rules with respect to one another (on by default)."] + True + normPercent = + expert $ + inGroup "Completion heuristics" $ + defaultFlag "normalise-queue-percent" "Percent of time spent renormalising queued critical pairs" cfg_renormalise_percent argNum + cpSampleSize = + expert $ + inGroup "Completion heuristics" $ + defaultFlag "cp-sample-size" "Size of random CP sample used to trigger renormalisation" cfg_cp_sample_size argNum + cpRenormaliseThreshold = + expert $ + inGroup "Completion heuristics" $ + defaultFlag "cp-renormalise-threshold" "Trigger renormalisation when this percentage of CPs can be simplified" cfg_renormalise_threshold argNum + lweight = + expert $ + inGroup "Critical pair weighting heuristics" $ + defaultFlag "lhs-weight" "Weight given to LHS of critical pair" (CP.cfg_lhsweight . cfg_critical_pairs) argNum + rweight = + expert $ + inGroup "Critical pair weighting heuristics" $ + defaultFlag "rhs-weight" "Weight given to RHS of critical pair" (CP.cfg_rhsweight . cfg_critical_pairs) argNum + funweight = + expert $ + inGroup "Critical pair weighting heuristics" $ + defaultFlag "fun-weight" "Weight given to function symbols" (CP.cfg_funweight . cfg_critical_pairs) argNum + varweight = + expert $ + inGroup "Critical pair weighting heuristics" $ + defaultFlag "var-weight" "Weight given to variable symbols" (CP.cfg_varweight . cfg_critical_pairs) argNum + depthweight = + expert $ + inGroup "Critical pair weighting heuristics" $ + defaultFlag "depth-weight" "Weight given to critical pair depth" (CP.cfg_depthweight . cfg_critical_pairs) argNum + dupcost = + expert $ + inGroup "Critical pair weighting heuristics" $ + defaultFlag "dup-cost" "Cost of duplicate subterms" (CP.cfg_dupcost . cfg_critical_pairs) argNum + dupfactor = + expert $ + inGroup "Critical pair weighting heuristics" $ + defaultFlag "dup-factor" "Size factor of duplicate subterms" (CP.cfg_dupfactor . cfg_critical_pairs) argNum + ground_join = + expert $ + inGroup "Critical pair joining heuristics" $ + bool "ground-joining" + ["Test terms for ground joinability (on by default)."] + True + connectedness = + expert $ + inGroup "Critical pair joining heuristics" $ + bool "connectedness" + ["Test terms for subconnectedness, as a separate check (on by default)."] + True + ground_connectedness = + expert $ + inGroup "Critical pair joining heuristics" $ + bool "ground-connectedness" + ["Test terms for subconnectedness, as part of ground joinability testing (off by default)."] + False + complete_subsets = + expert $ + inGroup "Critical pair joining heuristics" $ + bool "complete-subsets" + ["Identify and exploit complete subsets of the axioms in joining (off by default)."] + False + set_join = + expert $ + inGroup "Critical pair joining heuristics" $ + bool "set-join" + ["Compute all normal forms when joining critical pairs (off by default)."] + False + set_join_goals = + expert $ + inGroup "Critical pair joining heuristics" $ + bool "set-join-goals" + ["Compute all normal forms when joining goal terms (on by default)."] + True + always_simplify = + expert $ + inGroup "Debugging options" $ + bool "always-simplify" + ["Interreduce rules after every step."] + False + all_lemmas = + inGroup "Proof presentation" $ + bool "all-lemmas" + ["Produce a proof with one lemma for each critical pair (off by default)."] + False + flat_proof = + inGroup "Proof presentation" $ + bool "no-lemmas" + ["Produce a proof with no lemmas (off by default).", + "May lead to exponentially large proofs."] + False + ground_proof = + inGroup "Proof presentation" $ + bool "ground-proof" + ["Produce a ground proof (off by default).", + "May lead to exponentially large proofs."] + False + show_instances = + inGroup "Proof presentation" $ + bool "show-instances" + ["Show which instance of a lemma or axiom each rewrite step uses (off by default)."] + False + show_axiom_uses = + inGroup "Proof presentation" $ + interpret <$> + concat <$> + manyFlags "show-uses-of" + ["Show which instances of the given axioms were needed (none by default).", + "Separate multiple axiom names with commas.", + "Use --show-uses-of all to show uses of all axioms."] + (splitOn "," <$> arg "" "expected a list of axiom names" Just) + where + interpret xss ax = axiom_name ax `elem` xss || "all" `elem` xss + colour = fromMaybe <$> io colourSupported <*> colourFlag + colourFlag = + inGroup "Proof presentation" $ + primFlag "(no-)colour" + ["Produce output in colour (on by default if writing output to a terminal)."] + (`elem` map fst colourFlags) + (\_ y -> return y) + Nothing + (pure (`lookup` colourFlags)) + colourFlags = [("--colour", True), ("--no-colour", False), + ("--color", True), ("--no-color", False)] + colourSupported = + liftM2 (&&) (hSupportsANSIColor stdout) + (return (setSGRCode [] /= "")) -- Check for Windows terminal not supporting ANSI + + defaultFlag name desc field parser = + flag name [desc ++ " (" ++ show def ++ " by default)."] def parser + where + def = field defaultConfig + +parsePrecedence :: OptionParser [String] +parsePrecedence = + expert $ + inGroup "Term order options" $ + fmap (splitOn ",") + (flag "precedence" ["List of functions in descending order of precedence."] [] (arg "" "expected a function name" Just)) + +data Constant = + Minimal | + Constant { + con_prec :: {-# UNPACK #-} !Precedence, + con_id :: {-# UNPACK #-} !Jukebox.Function, + con_arity :: {-# UNPACK #-} !Int, + con_size :: !Integer, + con_weight :: !Integer, + con_bonus :: !Bool } + deriving (Eq, Ord) + +data Precedence = Precedence !Bool !Bool !(Maybe Int) !Int + deriving (Eq, Ord) + +instance Labelled Constant where + label = fromIntegral . Label.labelNum . Label.label + find = Label.find . Label.unsafeMkLabel . fromIntegral + +instance KBO.Sized Constant where + size Minimal = 1 + size Constant{..} = con_size +instance KBO.Weighted Constant where + argWeight Minimal = 1 + argWeight Constant{..} = con_weight +instance Arity Constant where + arity Minimal = 0 + arity Constant{..} = con_arity + +instance Pretty Constant where + pPrint Minimal = text "?" + pPrint Constant{..} = text (removePostfix (base con_id)) + where + removePostfix ('_':x:xs) | con_arity == 1 = x:xs + removePostfix xs = xs + +instance PrettyTerm Constant where + termStyle Minimal = uncurried + termStyle Constant{..} + | hasLabel "type_tag" con_id = invisible + | "_" `isPrefixOf` base con_id && con_arity == 1 = postfix + | any isAlphaNum (base con_id) = uncurried + | otherwise = + case con_arity of + 1 -> prefix + 2 -> infixStyle 5 + _ -> uncurried + +instance Minimal Constant where + minimal = fun Minimal + +instance Ordered Constant where + lessEq t u = KBO.lessEq t u + lessIn model t u = KBO.lessIn model t u + lessEqSkolem t u = KBO.lessEqSkolem t u + +instance EqualsBonus Constant where + hasEqualsBonus Minimal = False + hasEqualsBonus c = con_bonus c + isEquals Minimal = False + isEquals c = SequentialMain.isEquals (con_id c) + isTrue Minimal = False + isTrue c = SequentialMain.isTrue (con_id c) + isFalse Minimal = False + isFalse c = SequentialMain.isFalse (con_id c) + +data TweeContext = + TweeContext { + ctx_var :: Jukebox.Variable, + ctx_minimal :: Jukebox.Function, + ctx_true :: Jukebox.Function, + ctx_false :: Jukebox.Function, + ctx_equals :: Jukebox.Function, + ctx_type :: Type } + +-- Convert back and forth between Twee and Jukebox. +tweeConstant :: HornFlags -> TweeContext -> Precedence -> Jukebox.Function -> Constant +tweeConstant flags TweeContext{..} prec fun + | fun == ctx_minimal = Minimal + | otherwise = Constant prec fun (Jukebox.arity fun) (sz fun) 1 (bonus fun) + where + sz fun = {-if isType fun then 0 else-} 1 + bonus fun = + (isIfeq fun && encoding flags /= Asymmetric2) || + SequentialMain.isEquals fun + +isType :: Jukebox.Function -> Bool +isType fun = + hasLabel "type_tag" (name fun) && Jukebox.arity fun == 1 + +isIfeq :: Jukebox.Function -> Bool +isIfeq fun = + hasLabel "ifeq" (name fun) + +isEquals :: Jukebox.Function -> Bool +isEquals fun = + hasLabel "equals" (name fun) && Jukebox.arity fun == 2 + +isTrue :: Jukebox.Function -> Bool +isTrue fun = + hasLabel "true" (name fun) && Jukebox.arity fun == 0 + +isFalse :: Jukebox.Function -> Bool +isFalse fun = + hasLabel "false" (name fun) && Jukebox.arity fun == 0 + +jukeboxFunction :: TweeContext -> Constant -> Jukebox.Function +jukeboxFunction _ Constant{..} = con_id +jukeboxFunction TweeContext{..} Minimal = ctx_minimal + +tweeTerm :: HornFlags -> TweeContext -> (Jukebox.Function -> Precedence) -> Jukebox.Term -> Term Constant +tweeTerm flags ctx prec t = build (tm t) + where + tm (Jukebox.Var (x ::: _)) = + var (V (fromIntegral (Label.labelNum (Label.label x)))) + tm (f :@: ts) = + app (fun (tweeConstant flags ctx (prec f) f)) (map tm ts) + +jukeboxTerm :: TweeContext -> Term Constant -> Jukebox.Term +jukeboxTerm TweeContext{..} (Var (V x)) = + Jukebox.Var (Unique (fromIntegral x) (intern "X") Nothing defaultRenamer ::: ctx_type) +jukeboxTerm ctx@TweeContext{..} (App f t) = + jukeboxFunction ctx (fun_value f) :@: map (jukeboxTerm ctx) ts + where + ts = unpack t + +makeContext :: Problem Clause -> TweeContext +makeContext prob = run prob $ \prob -> do + let + ty = + case types' prob of + [] -> indType + [ty] -> ty + + var <- newSymbol "X" ty + minimal <- newFunction (withLabel "minimal" (name "constant")) [] ty + true <- newFunction (withLabel "true" (name "true")) [] ty + false <- newFunction (withLabel "false" (name "false")) [] ty + equals <- newFunction (withLabel "equals" (name "equals")) [ty, ty] ty + + return TweeContext { + ctx_var = var, + ctx_minimal = minimal, + ctx_true = true, + ctx_false = false, + ctx_equals = equals, + ctx_type = ty } + +flattenGoals :: Bool -> Bool -> Problem Clause -> Problem Clause +flattenGoals flattenAll full prob = + run prob $ \prob -> do + cs <- concat <$> mapM flatten prob + return $ + prob ++ + [ Input{tag = "flattening", kind = Jukebox.Ax Definition, + what = c, source = Unknown } + | c <- cs ] + where + flatten Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])} = + liftM2 (++) (flat x) (flat y) + flatten Input{what = Clause (Bind _ [Pos (x Jukebox.:=: y)])} + | flattenAll = + liftM2 (++) (flat x) (flat y) + flatten _ = return [] + + flat (f :@: ts) + | not (all isVar ts) || usort ts /= ts = do + name <- newName f + let vs = Jukebox.vars ts + g = name ::: FunType (map typ vs) (typ f) + c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: f :@: ts)] + css <- if full then concat <$> mapM flat ts else return [] + return (c:css) + flat _ = return [] + + isVar (Jukebox.Var _) = True + isVar _ = False + +-- Encode existentials so that all goals are ground. +addNarrowing :: TweeContext -> Problem Clause -> Problem Clause +addNarrowing TweeContext{..} prob = + unchanged ++ equalityClauses + where + (unchanged, nonGroundGoals) = partitionEithers (map f prob) + where + f inp@Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])} + | not (ground x) || not (ground y) = + Right (inp, (x, y)) + f inp = Left inp + + equalityClauses + | null nonGroundGoals = [] + | otherwise = + -- Turn a != b & c != d & ... + -- into eq(a,b)=false & eq(c,d)=false & eq(X,X)=true & true!=false (esa) + -- and then extract the individual components (thm) + let + equalityLiterals = + -- true != false + ("true_equals_false", Neg ((ctx_true :@:) [] Jukebox.:=: (ctx_false :@: []))): + -- eq(X,X)=true + ("reflexivity", Pos (ctx_equals :@: [Jukebox.Var ctx_var, Jukebox.Var ctx_var] Jukebox.:=: (ctx_true :@: []))): + -- [eq(a,b)=false, eq(c,d)=false, ...] + [ (tag, Pos (ctx_equals :@: [x, y] Jukebox.:=: (ctx_false :@: []))) + | (Input{tag = tag}, (x, y)) <- nonGroundGoals ] + + -- Equisatisfiable to the input clauses + justification = + Input { + tag = "new_negated_conjecture", + kind = Jukebox.Ax NegatedConjecture, + what = + let form = And (map (Literal . snd) equalityLiterals) in + ForAll (Bind (Set.fromList (vars form)) form), + source = + Inference "encode_existential" "esa" + (map (fmap toForm . fst) nonGroundGoals) } + + input tag form = + Input { + tag = tag, + kind = Conj Conjecture, + what = clause [form], + source = + Inference "split_conjunct" "thm" [justification] } + + in [input tag form | (tag, form) <- equalityLiterals] + +data PreEquation = + PreEquation { + pre_name :: String, + pre_form :: Input Form, + pre_eqn :: (Jukebox.Term, Jukebox.Term) } + +-- Split the problem into axioms and ground goals. +identifyProblem :: + TweeContext -> Problem Clause -> Either (Input Clause) ([PreEquation], [PreEquation]) +identifyProblem TweeContext{..} prob = + fmap partitionEithers (mapM identify prob) + + where + pre inp x = + PreEquation { + pre_name = tag inp, + pre_form = fmap toForm inp, + pre_eqn = x } + + identify inp@Input{what = Clause (Bind _ [Pos (t Jukebox.:=: u)])} = + return $ Left (pre inp (t, u)) + identify inp@Input{what = Clause (Bind _ [Neg (t Jukebox.:=: u)])} + | ground t && ground u = + return $ Right (pre inp (t, u)) + identify inp@Input{what = Clause (Bind _ [])} = + -- The empty clause can appear after clausification if + -- the conjecture was trivial + return $ Left (pre inp (Jukebox.Var ctx_var, ctx_minimal :@: [])) + identify inp = Left inp + +runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> MainFlags -> (IO () -> IO ()) -> Problem Clause -> IO Answer +runTwee globals (TSTPFlags tstp) horn precedence config MainFlags{..} later obligs = {-# SCC runTwee #-} do + let + -- Encode whatever needs encoding in the problem + obligs' + | flags_flatten_goals_lightly = flattenGoals False False obligs + | flags_flatten_all = flattenGoals True True obligs + | flags_flatten_goals = flattenGoals False True obligs + | otherwise = obligs + ctx = makeContext obligs' + lowercaseSkolem x + | hasLabel "skolem" x = + withRenamer x $ \s i -> + case defaultRenamer s i of + Renaming xss xs -> + Renaming (map (map toLower) xss) (map toLower xs) + | otherwise = x + prob = prettyNames (mapName lowercaseSkolem (addNarrowing ctx obligs')) + + (axioms0, goals0) <- + case identifyProblem ctx prob of + Left inp -> do + mapM_ (hPutStrLn stderr) [ + "The problem contains the following clause, which is not a unit equality:", + indent (show (pPrintClauses [inp])), + "Twee only handles unit equality problems."] + exitWith (ExitFailure 1) + Right x -> return x + + let + -- Work out a precedence for function symbols + prec c = + Precedence + (isType c) + (isNothing (elemIndex (base c) precedence)) + (fmap negate (elemIndex (base c) precedence)) + (maybeNegate (Map.findWithDefault 0 c occs)) + maybeNegate = if flags_flip_ordering then negate else id + occs = funsOcc prob + + -- Translate everything to Twee. + toEquation (t, u) = + canonicalise (tweeTerm horn ctx prec t :=: tweeTerm horn ctx prec u) + + goals = + [ goal n pre_name (toEquation pre_eqn) + | (n, PreEquation{..}) <- zip [1..] goals0 ] + axioms = + [ Axiom n pre_name (toEquation pre_eqn) + | (n, PreEquation{..}) <- zip [1..] (sortBy axiomCompare axioms0) ] + defs = + [ axiom + | (axiom, PreEquation{..}) <- zip axioms (sortBy axiomCompare axioms0), + isDefinition pre_form ] + isDefinition Input{source = Unknown} = True + isDefinition inp = tag inp `elem` flags_eliminate + axiomCompare ax1 ax2 + | ax1' `simplerThan` ax2' = LT + | ax2' `simplerThan` ax1' = GT + | otherwise = EQ + where + ax1' = toEquation (pre_eqn ax1) + ax2' = toEquation (pre_eqn ax2) + + withGoals = foldl' (addGoal config) (initialState config) goals + withAxioms = foldl' (addAxiom config) withGoals axioms + withBackwardsGoal = foldn rewriteGoalsBackwards withAxioms flags_backwards_goal + + -- Set up tracing. + sayTrace <- + case flags_trace of + Nothing -> return $ \_ -> return () + Just (file, mod) -> do + h <- openFile file WriteMode + hSetBuffering h LineBuffering + let put msg = hPutStrLn h msg + put $ ":- module(" ++ mod ++ ", [step/1, lemma/1, axiom/1, goal/1])." + put ":- discontiguous(step/1)." + put ":- discontiguous(lemma/1)." + put ":- discontiguous(axiom/1)." + put ":- discontiguous(goal/1)." + put ":- style_check(-singleton)." + return $ \msg -> hPutStrLn h msg + + let + say msg = unless (quiet globals) (putStrLn msg) + line = say "" + output = Output { + output_message = \msg -> do + say (prettyShow msg) + sayTrace (show (traceMsg msg)) } + + traceMsg (NewActive active) = + step "add" [traceActive active] + traceMsg (NewEquation eqn) = + step "hard" [traceEqn eqn] + traceMsg (DeleteActive active) = + step "delete" [traceActive active] + traceMsg SimplifyQueue = + step "simplify_queue" [] + traceMsg Interreduce = + step "interreduce" [] + traceMsg (Status n) = + step "status" [pPrint n] + + traceActive Active{active_top = Nothing, ..} = + traceApp "rule" [pPrint active_id, traceEqn (unorient active_rule)] + traceActive Active{active_top = Just top, ..} = + traceApp "rule" [pPrint active_id, traceEqn (unorient active_rule), traceEqn lemma1, traceEqn lemma2] + where + (lemma1, lemma2) = + find (steps (derivation active_proof)) + find (s1:s2:_) + | eqn_rhs (equation (certify s1)) == top && eqn_lhs (equation (certify s2)) == top = + (lemmaOf s1, lemmaOf s2) + find (_:xs) = find xs + lemmaOf s = + case (usedLemmas s, usedAxioms s) of + ([p], []) -> equation p + ([], [ax]) -> axiom_eqn ax + + traceEqn (t :=: u) = + pPrintPrec prettyNormal 6 t <+> text "=" <+> pPrintPrec prettyNormal 6 u + traceApp f xs = + pPrintTerm uncurried prettyNormal 0 (text f) xs + + step :: String -> [Doc] -> Doc + step f xs = traceApp "step" [traceApp f xs] <#> text "." + + say "Here is the input problem:" + forM_ axioms $ \Axiom{..} -> + say $ show $ nest 2 $ + describeEquation "Axiom" + (show axiom_number) (Just axiom_name) axiom_eqn + forM_ goals $ \Goal{..} -> + say $ show $ nest 2 $ + describeEquation "Goal" + (show goal_number) (Just goal_name) goal_eqn + line + + state <- complete output config withBackwardsGoal + line + + when (solved state && flags_proof) $ later $ do + let + cfg_present + | tstp && flags_formal_proof = + (cfg_proof_presentation config){cfg_all_lemmas = True} + | otherwise = + cfg_proof_presentation config + pres = present cfg_present $ map (eliminateDefinitionsFromGoal defs) $ solutions state + + sayTrace "" + forM_ (pres_axioms pres) $ \p -> + sayTrace $ show $ + traceApp "axiom" [traceEqn (axiom_eqn p)] <#> text "." + forM_ (pres_lemmas pres) $ \p -> + sayTrace $ show $ + traceApp "lemma" [traceEqn (equation p)] <#> text "." + forM_ (pres_goals pres) $ \p -> + sayTrace $ show $ + traceApp "goal" [traceEqn (pg_goal_hint p)] <#> text "." + + when (tstp && not flags_formal_proof) $ do + putStrLn "% SZS output start Proof" + let + axiomForms = + Map.fromList + (zip (map axiom_number axioms) (map pre_form axioms0)) + goalForms = + Map.fromList + (zip (map goal_number goals) (map pre_form goals0)) + + findSource forms n = + case Map.lookup n forms of + Nothing -> [] + Just inp -> go inp + where + go Input{source = Unknown} = [] + go Input{source = Inference _ _ inps} = concatMap go inps + go inp@Input{source = FromFile _ _} = [inp] + + when flags_explain_encoding $ do + putStrLn "Take the following subset of the input axioms:" + mapM_ putStrLn $ map (" " ++) $ lines $ showProblem $ + usortBy (comparing show) $ + (pres_axioms pres >>= findSource axiomForms . axiom_number) ++ + (pres_goals pres >>= findSource goalForms . pg_number) + + putStrLn "" + putStrLn "Now clausify the problem and encode Horn clauses using encoding 3 of" + putStrLn "http://www.cse.chalmers.se/~nicsma/papers/horn.pdf." + putStrLn "We repeatedly replace C & s=t => u=v by the two clauses:" + putStrLn " fresh(y, y, x1...xn) = u" + putStrLn " C => fresh(s, t, x1...xn) = v" + putStrLn "where fresh is a fresh function symbol and x1..xn are the free" + putStrLn "variables of u and v." + putStrLn "A predicate p(X) is encoded as p(X)=true (this is sound, because the" + putStrLn "input problem has no model of domain size 1)." + putStrLn "" + putStrLn "The encoding turns the above axioms into the following unit equations and goals:" + putStrLn "" + print $ pPrintPresentation (cfg_proof_presentation config) pres + putStrLn "% SZS output end Proof" + putStrLn "" + + when (tstp && flags_formal_proof) $ do + putStrLn "% SZS output start CNFRefutation" + print $ pPrintProof $ + presentToJukebox ctx (curry toEquation) + (zip (map axiom_number axioms) (map pre_form axioms0)) + (zip (map goal_number goals) (map pre_form goals0)) + pres + putStrLn "% SZS output end CNFRefutation" + putStrLn "" + + unless tstp $ do + putStrLn "The conjecture is true! Here is a proof." + putStrLn "" + print $ pPrintPresentation (cfg_proof_presentation config) pres + putStrLn "" + + when (not (quiet globals) && not (solved state)) $ later $ do + let + state' = interreduce config state + score rule = + (KBO.size (lhs rule), lhs rule, + KBO.size (rhs rule), rhs rule) + actives = + sortBy (comparing (score . active_rule)) $ + IntMap.elems (st_active_ids state') + + when (tstp && configIsComplete config) $ do + putStrLn "% SZS output start Saturation" + print $ pPrintProof $ + map pre_form axioms0 ++ + map pre_form goals0 ++ + [ Input "rule" (Jukebox.Ax Jukebox.Axiom) Unknown $ + toForm $ clause + [Pos (jukeboxTerm ctx (lhs rule) Jukebox.:=: jukeboxTerm ctx (rhs rule))] + | rule <- rules state ] + putStrLn "% SZS output end Saturation" + putStrLn "" + + if configIsComplete config then do + putStrLn "Ran out of critical pairs. This means the conjecture is not true." + else do + putStrLn "Gave up on reaching the given resource limit." + putStrLn "Here is the final rewrite system:" + forM_ actives $ \active -> + putStrLn (" " ++ prettyShow (canonicalise (active_rule active))) + putStrLn "" + + return $ + if solved state then Unsat Unsatisfiable Nothing + else if configIsComplete config && not (dropNonHorn horn) && not flags_give_up_on_saturation then Sat Satisfiable Nothing + else NoAnswer GaveUp + +-- Transform a proof presentation into a Jukebox proof. +presentToJukebox :: + TweeContext -> + (Jukebox.Term -> Jukebox.Term -> Equation Constant) -> + -- Axioms, indexed by axiom number. + [(Int, Input Form)] -> + -- N.B. the formula here proves the negated goal. + [(Int, Input Form)] -> + Presentation Constant -> + Problem Form +presentToJukebox ctx toEquation axioms goals Presentation{..} = + [ Input { + tag = pg_name, + kind = Jukebox.Ax Jukebox.Axiom, + what = false, + source = + Inference "resolution" "thm" + [-- A proof of t != u + existentialHack pg_goal_hint (fromJust (lookup pg_number goals)), + -- A proof of t = u + fromJust (Map.lookup pg_number goal_proofs)] } + | ProvedGoal{..} <- pres_goals ] + + where + axiom_proofs = + Map.fromList + [ (axiom_number, fromJust (lookup axiom_number axioms)) + | Axiom{..} <- pres_axioms ] + + lemma_proofs = + Map.fromList [(p, tstp p) | p <- pres_lemmas] + + goal_proofs = + Map.fromList [(pg_number, tstp pg_proof) | ProvedGoal{..} <- pres_goals] + + tstp :: Proof Constant -> Input Form + tstp = deriv . derivation + + deriv :: Derivation Constant -> Input Form + deriv p@(Trans q r) = derivFrom (deriv r:sources q) p + deriv p = derivFrom (sources p) p + + derivFrom :: [Input Form] -> Derivation Constant -> Input Form + derivFrom sources p = + Input { + tag = "step", + kind = Jukebox.Ax Jukebox.Axiom, + what = jukeboxEquation (equation (certify p)), + source = + Inference "rw" "thm" sources } + + jukeboxEquation :: Equation Constant -> Form + jukeboxEquation (t :=: u) = + toForm $ clause [Pos (jukeboxTerm ctx t Jukebox.:=: jukeboxTerm ctx u)] + + sources :: Derivation Constant -> [Input Form] + sources p = + [ fromJust (Map.lookup lemma lemma_proofs) + | lemma <- usort (usedLemmas p) ] ++ + [ fromJust (Map.lookup axiom_number axiom_proofs) + | Axiom{..} <- usort (usedAxioms p) ] + + -- An ugly hack: since Twee.Proof decodes $true = $false into a + -- proof of the existentially quantified goal, we need to do the + -- same decoding at the Jukebox level. + existentialHack eqn input = + case find input of + [] -> error $ "bug in TSTP output: can't fix up decoded existential" + (inp:_) -> inp + where + -- Check if this looks like the correct clause; + -- if not, try its ancestors. + find inp | ok inp = [inp] + find Input{source = Inference _ _ inps} = + concatMap find inps + find _ = [] + + ok inp = + case toClause (what inp) of + Nothing -> False + Just (Clause (Bind _ [Neg (t' Jukebox.:=: u')])) -> + let + eqn' = toEquation t' u' + ts = buildList [eqn_lhs eqn, eqn_rhs eqn] + us = buildList [eqn_lhs eqn', eqn_rhs eqn'] + in + isJust (matchList ts us) && isJust (matchList us ts) + +main = do + hSetBuffering stdout LineBuffering + join . parseCommandLineWithExtraArgs + ["--no-conjunctive-conjectures", "--no-split"] +#ifdef VERSION_twee + "Twee, an equational theorem prover" . version ("twee version " ++ VERSION_twee) $ +#else + "Twee, an equational theorem prover" . version "twee development version" $ +#endif + globalFlags *> parseMainFlags *> + -- hack: get --quiet and --no-proof options to appear before --tstp + forAllFilesBox <*> + (readProblemBox =>>= + expert clausifyBox =>>= + forAllConjecturesBox <*> + (combine <$> + expert hornToUnitBox <*> + parseConfig <*> + parseMainFlags <*> + (toFormulasBox =>>= + expert (toFof <$> clausifyBox <*> pure (tags True)) =>>= + expert clausifyBox =>>= expert oneConjectureBox) <*> + (runTwee <$> globalFlags <*> tstpFlags <*> expert hornFlags <*> parsePrecedence))) + where + combine horn config main encode prove later prob0 = do + res <- horn prob0 + case res of + Left ans -> return ans + Right prob -> do + let + isUnitEquality [Pos (_ Jukebox.:=: _)] = True + isUnitEquality [Neg (_ Jukebox.:=: _)] = True + isUnitEquality _ = False + isUnit = all isUnitEquality (map (toLiterals . what) prob0) + main' = if isUnit then main else main{flags_formal_proof = False} + encode prob >>= prove config main' later diff --git a/misc/BestTwee.hs b/misc/BestTwee.hs new file mode 100644 --- /dev/null +++ b/misc/BestTwee.hs @@ -0,0 +1,157 @@ +import MaxCover +import System.FilePath +import System.FilePath.Glob +import System.Directory +import Control.Monad +import Data.Ord +import Data.List +import Data.Maybe +import Data.Time.Clock + +solvedInTime :: NominalDiffTime -> FilePath -> String -> IO Bool +solvedInTime timeLimit dir prob = do + let + stdout = dir prob ++ ".p.stdout" + stderr = dir prob ++ ".p.stderr" + outTime <- getModificationTime stdout + errTime <- getModificationTime stderr + return (diffUTCTime outTime errTime <= timeLimit) + +notE :: [(String, Double)] +notE = [ + ("LAT168-1", 0.30), ("LAT171-1", 0.43), ("ALG240-1", 0.48), ("LAT174-1", 0.65), ("GRP768-1", 0.70), + ("LAT142-1", 0.70), ("GRP505-1", 0.74), ("LAT145-1", 0.74), ("LAT164-1", 0.74), ("RNG025-5", 0.74), + ("GRP506-1", 0.78), ("GRP507-1", 0.78), ("LAT018-1", 0.78), ("LAT148-1", 0.78), ("LAT153-1", 0.78), + ("LAT155-1", 0.78), ("RNG025-4", 0.78), ("GRP508-1", 0.83), ("KLE151-10", 0.83), ("LAT162-1", 0.83), + ("ALG246-1", 0.87), ("GRP024-5", 0.87), ("GRP766-1", 0.87), ("LAT146-1", 0.87), ("LAT159-1", 0.87), + ("LAT160-1", 0.87), ("LAT170-1", 0.87), ("LAT177-1", 0.87), ("REL022-2", 0.87), ("COL042-10", 0.91), + ("GRP196-1", 0.91), ("GRP666-3", 0.91), ("GRP666-4", 0.91), ("GRP666-5", 0.91), ("LAT156-1", 0.91), + ("LAT157-1", 0.91), ("LAT169-1", 0.91), ("LCL148-10", 0.91), ("REL020-2", 0.91), ("REL021-1", 0.91), + ("REL021-2", 0.91), ("REL022-1", 0.91), ("REL029-1", 0.91), ("REL033-1", 0.91), ("REL033-3", 0.91), + ("REL034-1", 0.91), ("REL034-2", 0.91), ("REL035-1", 0.91), ("REL035-2", 0.91), ("REL036-1", 0.91), + ("GRP164-1", 0.96), ("GRP164-2", 0.96), ("GRP666-2", 0.96), ("GRP678-1", 0.96), ("GRP721-1", 0.96), + ("GRP725-1", 0.96), ("KLE110-10", 0.96), ("LAT072-1", 0.96), ("LAT076-1", 0.96), ("LAT140-1", 0.96), + ("LAT141-1", 0.96), ("LAT144-1", 0.96), ("LAT147-1", 0.96), ("LAT149-1", 0.96), ("LAT151-1", 0.96), + ("LAT158-1", 0.96), ("LAT163-1", 0.96), ("LAT167-1", 0.96), ("LAT172-1", 0.96), ("LAT173-1", 0.96), + ("LAT175-1", 0.96), ("LAT176-1", 0.96), ("LAT183-10", 0.96), ("LAT186-10", 0.96), ("LCL927-10", 0.96), + ("REL020-1", 0.96), ("REL040-1", 0.96), ("REL040-3", 0.96), ("GRP177-1", 1.00), ("GRP724-1", 1.00), + ("LAT074-1", 1.00), ("LAT075-1", 1.00), ("LAT077-1", 1.00), ("LAT078-1", 1.00), ("LAT079-1", 1.00), + ("LAT139-1", 1.00), ("LAT161-1", 1.00), ("LCL220-10", 1.00), ("LCL330-10", 1.00), ("LCL348-10", 1.00), + ("REL032-1", 1.00), ("REL032-2", 1.00), ("REL038-1", 1.00), ("REL039-1", 1.00), ("ROB007-1", 1.00), + ("ROB033-1", 1.00)] + +problemBonus :: (Int, Int, Int, Int, Int, Int) -> String -> Int +problemBonus (b0, b1, b2, b3, b4, b5) p = + case lookup p notE of + Nothing -> b0 + Just x + | x < 0.7 -> b1 + | x < 0.8 -> b2 + | x < 0.9 -> b3 + | x < 0.95 -> b4 + | otherwise -> b5 + +greatProblemsBonus :: (Int, Int, Int, Int, Int, Int) -> String -> [String] +greatProblemsBonus b p = + [p ++ "/" ++ show i | i <- [1..problemBonus b p]] + +bonuses :: [(String, (Int, Int, Int, Int, Int, Int))] +bonuses = + [("no bonus", (1, 1, 1, 1, 1, 1)), + ("low bonus", (1, 1, 2, 3, 4, 5)), + ("medium bonus", (1, 2, 4, 6, 8, 10)), + ("high bonus", (0, 1, 2, 3, 4, 5)), + ("big fish", (0, 0, 0, 0, 1, 1))] + +readResults ok = do + filenames <- glob "out/twee-*/success" + fmap (filter (\(x, _) -> x `notElem` banned)) $ forM filenames $ \filename -> do + let directory = takeDirectory filename + let name = takeFileName directory + solved <- fmap (filter ok) $ lines <$> readFile filename + fast <- filterM (solvedInTime 120 directory) solved + slow <- filterM (solvedInTime 600 directory) solved + return (name, (fast, slow)) + +score results cover = + length (usort (concat [probs | (name, probs) <- results, name `elem` cover])) + +levels results name names = + [ (i, length xs) + | i <- [0..length names], + let xs = find name \\ concatMap find (take i names), + not (null xs) ] + where + find x = fromJust (lookup x results) + +main = do + probs <- lines <$> readFile "casc-j10" + results <- readResults (`elem` probs) + let + options = + [("fast", \(fast, _) -> (fast, []))] + --("slow", \(_, slow) -> ([], slow)), + --("fast and slow", id)] + + forM_ options $ \(option, f) -> do + forM_ bonuses $ \(bonus, b) -> do + let + results1 = + [ (name, + map (++ "/fast") (concatMap (greatProblemsBonus b) fast) ++ + map (++ "/slow") (concatMap (greatProblemsBonus b) slow)) + | (name, res) <- results, + let (fast, slow) = f res ] + + best = greedy results1 + + putStrLn (option ++ "/" ++ bonus ++ ":") + forM_ (zip3 [1..] best (inits best)) $ \(i, name, names) -> do + putStrLn (show i ++ ". " ++ name ++ " " ++ show (score results1 (name:names)) ++ ", useful at levels " ++ show (levels results1 name names)) + + putStrLn "" + +-- putStrLn "\nBest:" +-- forM_ [1..8] $ \i -> do +-- cover <- maxCover i results1 +-- putStrLn (show i ++ ": " ++ show (score results1 cover)) +-- forM_ cover $ \name -> putStrLn (" " ++ name) + +greedy [] = [] +greedy results = + best: + greedy (map deleteResults (delete (best, probs) results)) + where + (best, probs) = maximumBy (comparing f) results + deleteResults (name, probs') = (name, probs' \\ probs) + + f (name, probs) = + case elemIndex name fixed of + Just i -> Right (-i) + Nothing -> Left (length probs) + +fixed :: [String] +fixed = [ + "twee-200715-twee-goal-flip-lhs2", + "twee-200714-twee-goalagain", + "twee-200712-twee-ghc8.10", + "twee-200714-twee-goalagain-flip-lhs1", + "twee-200715-twee-goal-lhs4-var3", + "twee-200715-twee-goal-lhs6-var3", + "twee-200715-twee-goal-lhs2-var3", + "twee-200611-twee-flip-lhs9"] +--fixed = [ +-- "twee-200612-twee-aggressive-renormalise-flip-lhs4", +-- "twee-200612-twee-aggressive-renormalise-flip-lhs9", +-- "twee-200611-twee-flip-lhs1", +-- "twee-200611-twee-lhs4", +-- "twee-200611-twee-lhs5", +-- "twee-200612-twee-aggressive-renormalise-nodup", +-- "twee-200611-twee-nosimp", +-- "twee-200612-twee-aggressive-renormalise-nodepth"] + +banned :: [String] +banned = [] +-- "twee-200714-twee-goalagain", +-- "twee-200714-twee-goalagain-flip-lhs1", +-- "twee-200714-twee-goalagain-flip-lhs3"] diff --git a/misc/Localise.hs b/misc/Localise.hs new file mode 100644 --- /dev/null +++ b/misc/Localise.hs @@ -0,0 +1,114 @@ +import System.Process + +runTwee :: [String] -> [String] -> String -> IO Bool +runTwee args axioms conj = do + output <- + readProcess "/home/nick/.local/bin/twee" + ("--quiet":"--no-proof":"--max-cps":"20000":"/dev/stdin":args) + (unlines $ map axiom axioms ++ [conjecture conj]) + let + res = + case lines output of + ["RESULT: Unsatisfiable (the axioms are contradictory)."] -> + True + ["RESULT: Theorem (the conjecture is true)."] -> + True + ["RESULT: GaveUp (couldn't solve the problem)."] -> + False + _ -> + error output + + putStrLn (show (length axioms) ++ " => " ++ show res) + return res + +good, bad :: [String] +good = ["--no-simplify"] +bad = ["--always-simplify"] + +axiom, conjecture :: String -> String +axiom xs = "cnf(axiom, axiom, " ++ xs ++ ")." +conjecture xs = "cnf(conjecture, conjecture, " ++ xs ++ ")." + +simplifyConjecture :: [String] -> [String] -> String -> IO ([String], String) +simplifyConjecture axioms lemmas conjecture = do + res <- loop (reverse lemmas) + case res of + Nothing -> + return (lemmas, conjecture) + Just (lemmas, conjecture) -> + return (reverse lemmas, conjecture) + where + loop [] = return Nothing + loop (lemma:lemmas) = do + res <- loop lemmas + case res of + Just (lemmas, conjecture) -> + return (Just (lemmas, conjecture)) + Nothing -> do + res <- runTwee bad axioms lemma + case res of + True -> return Nothing + False -> return (Just (lemmas, lemma)) + +maximiseAxioms :: [String] -> [String] -> String -> IO [String] +maximiseAxioms axioms lemmas conjecture = loop [] (reverse lemmas) + where + loop axioms' [] = return (axioms ++ axioms') + loop axioms' (lemma:lemmas) = do + res <- runTwee bad (axioms ++ axioms' ++ [lemma]) conjecture + case res of + False -> + loop (lemma:axioms') lemmas + True -> + loop axioms' lemmas + +minimiseAxioms :: [String] -> String -> IO [String] +minimiseAxioms axioms conjecture = loop [] axioms + where + loop axioms [] = return (reverse axioms) + loop axioms (axiom:axioms') = do + res <- runTwee good (axioms ++ axioms') conjecture + case res of + True -> do + res <- runTwee bad (axioms ++ axioms') conjecture + case res of + False -> + loop axioms axioms' + True -> + loop (axiom:axioms) axioms' + False -> + loop (axiom:axioms) axioms' + +selectAxiom :: [String] -> [String] -> String -> IO String +selectAxiom axioms axioms' conjecture = loop axioms + where + loop [] = error "no axiom worked" + loop (axiom:axioms) = do + res <- runTwee good (axiom:axioms') conjecture + case res of + True -> do + res <- runTwee bad (axiom:axioms') conjecture + case res of + False -> + return axiom + True -> + loop axioms + False -> + loop axioms + +reduceAxioms :: [String] -> [String] -> String -> IO [String] +reduceAxioms axioms lemmas conjecture = loop [] axioms + where + loop chosen [] = return chosen + loop chosen (axiom:axioms) = do + axiom' <- selectAxiom (reverse lemmas ++ [axiom]) (chosen ++ axioms) conjecture + loop (axiom':chosen) axioms + +minimise :: IO [String] +minimise = do + axioms <- lines <$> readFile "axioms.p" + lemmas <- lines <$> readFile "lemmas.p" + [conjecture] <- lines <$> readFile "conjecture.p" + axioms' <- reduceAxioms axioms lemmas conjecture + writeFile "axioms2.p" (unlines axioms') + return axioms' diff --git a/misc/MaxCover.hs b/misc/MaxCover.hs new file mode 100644 --- /dev/null +++ b/misc/MaxCover.hs @@ -0,0 +1,63 @@ +module MaxCover where + +import SAT +import SAT.Optimize +import SAT.Unary hiding (modelValue) +import qualified SAT.Unary as Unary +import Data.List +import qualified Data.Map.Strict as Map +import Control.Monad + +usort :: Ord a => [a] -> [a] +usort = map head . group . sort + +maxCover :: (Ord label, Ord object) => Int -> [(label, [object])] -> IO [label] +maxCover limit xs = do + s <- newSolver + let + labels = map fst xs + objects = usort (concatMap snd xs) + + labelLits <- sequence [newLit s | _ <- labels] + objectLits <- sequence [newLit s | _ <- objects] + + let + labelMap = Map.fromList (zip labels labelLits) + labelInvMap = Map.fromList (zip labelLits labels) + objectMap = Map.fromList (zip objects objectLits) + find m x = Map.findWithDefault undefined x m + + lits <- + maxCover_ s limit + [ (find labelMap label, map (find objectMap) objects) + | (label, objects) <- xs ] + + return (map (find labelInvMap) lits) + +maxCover_ :: Solver -> Int -> [(Lit, [Lit])] -> IO [Lit] +maxCover_ s limit xs = do + let + labels = map fst xs + objects = usort (concatMap snd xs) + occ = Map.fromListWith (++) [(obj, [label]) | (label, objs) <- xs, obj <- objs] + + forM_ xs $ \(label, objs) -> do + forM_ objs $ \obj -> do + addClause s [neg label, obj] + + forM_ objects $ \obj -> do + let labels = Map.findWithDefault undefined obj occ + addClause s (neg obj:labels) + + numChosen <- count s labels + numCovered <- count s objects + + -- Maximise #objects while respecting limit + addClause s [numChosen .<= limit] + True <- solveMaximize s [] numCovered + + -- Now minimise #labels while preserving #objects + goal <- Unary.modelValue s numCovered + addClause s [numCovered .>= goal] + True <- solveMinimize s [] numChosen + filterM (modelValue s) labels diff --git a/tests/GRP666-4.p b/tests/GRP666-4.p new file mode 100644 --- /dev/null +++ b/tests/GRP666-4.p @@ -0,0 +1,63 @@ +%------------------------------------------------------------------------------ +% File : GRP666-4 : TPTP v7.2.0. Released v4.0.0. +% Domain : Group Theory (Quasigroups) +% Problem : Inverse property A-loops are Moufang +% Version : Especial. +% English : + +% Refs : [KKP02] Kinyon et al. (2002), Every Diassociative A-loop is M +% : [PS08] Phillips & Stanovsky (2008), Automated Theorem Proving +% : [Sta08] Stanovsky (2008), Email to G. Sutcliffe +% Source : [Sta08] +% Names : KKP02a [PS08] + +% Status : Unsatisfiable +% Rating : 0.84 v7.1.0, 0.83 v7.0.0, 0.89 v6.3.0, 0.82 v6.2.0, 0.71 v6.1.0, 0.81 v5.5.0, 0.84 v5.4.0, 0.87 v5.3.0, 0.75 v5.2.0, 0.86 v5.1.0, 0.87 v5.0.0, 0.86 v4.1.0, 0.82 v4.0.1, 0.86 v4.0.0 +% Syntax : Number of clauses : 12 ( 0 non-Horn; 12 unit; 1 RR) +% Number of atoms : 12 ( 12 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 8 ( 4 constant; 0-2 arity) +% Number of variables : 25 ( 0 singleton) +% Maximal term depth : 5 ( 3 average) +% SPC : CNF_UNS_RFO_PEQ_UEQ + +% Comments : +%------------------------------------------------------------------------------ +cnf(c01,axiom, + ( mult(A,ld(A,B)) = B )). + +cnf(c02,axiom, + ( ld(A,mult(A,B)) = B )). + +cnf(c03,axiom, + ( mult(rd(A,B),B) = A )). + +cnf(c04,axiom, + ( rd(mult(A,B),B) = A )). + +cnf(c05,axiom, + ( mult(A,unit) = A )). + +cnf(c06,axiom, + ( mult(unit,A) = A )). + +cnf(c07,axiom, + ( ld(mult(A,B),mult(A,mult(B,mult(C,D)))) = mult(ld(mult(A,B),mult(A,mult(B,C))),ld(mult(A,B),mult(A,mult(B,D)))) )). + +cnf(c08,axiom, + ( rd(mult(mult(mult(A,B),C),D),mult(C,D)) = mult(rd(mult(mult(A,C),D),mult(C,D)),rd(mult(mult(B,C),D),mult(C,D))) )). + +cnf(c09,axiom, + ( ld(A,mult(mult(B,C),A)) = mult(ld(A,mult(B,A)),ld(A,mult(C,A))) )). + +cnf(c10,axiom, + ( mult(i(A),mult(A,B)) = B )). + +cnf(c11,axiom, + ( mult(mult(A,B),i(B)) = A )). + +cnf(goals,negated_conjecture, + ( mult(mult(a,b),mult(c,a)) != mult(mult(a,mult(b,c)),a) )). + +%------------------------------------------------------------------------------ diff --git a/tests/LAT071-1.p b/tests/LAT071-1.p new file mode 100644 --- /dev/null +++ b/tests/LAT071-1.p @@ -0,0 +1,37 @@ +%-------------------------------------------------------------------------- +% File : LAT071-1 : TPTP v7.2.0. Released v2.6.0. +% Domain : Lattice Theory (Orthomodularlattices) +% Problem : Given single axiom OML-21C, prove associativity +% Version : [MRV03] (equality) axioms. +% English : Given a single axiom candidate OML-21C for orthomodular lattices +% (OML) in terms of the Sheffer Stroke, prove a Sheffer stroke form +% of associativity. + +% Refs : [MRV03] McCune et al. (2003), Sheffer Stroke Bases for Ortholatt +% Source : [MRV03] +% Names : OML-21C-associativity [MRV03] + +% Status : Open +% Rating : 1.00 v2.6.0 +% Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) +% Number of atoms : 2 ( 2 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 4 ( 3 constant; 0-2 arity) +% Number of variables : 4 ( 2 singleton) +% Maximal term depth : 6 ( 4 average) +% SPC : CNF_OPN_RFO_PEQ_UEQ + +% Comments : +%-------------------------------------------------------------------------- +%----Single axiom OML-21C +cnf(oml_21C,axiom, + ( f(f(B,A),f(f(f(f(B,A),A),f(C,A)),f(f(A,A),D))) = A )). + +%----Denial of Sheffer stroke associativity +cnf(associativity,negated_conjecture, + ( f(a,f(f(b,c),f(b,c))) != f(c,f(f(b,a),f(b,a))) )). + +cnf(bonus, axiom, f(A,B)=f(B,A)). + +%-------------------------------------------------------------------------- diff --git a/tests/LAT073-1.p b/tests/LAT073-1.p new file mode 100644 --- /dev/null +++ b/tests/LAT073-1.p @@ -0,0 +1,37 @@ +%-------------------------------------------------------------------------- +% File : LAT073-1 : TPTP v7.2.0. Released v2.6.0. +% Domain : Lattice Theory (Ortholattices) +% Problem : Given single axiom MOL-23C, prove modularity +% Version : [MRV03] (equality) axioms. +% English : Given a single axiom candidate MOL-23C for modular ortholattices +% (MOL) in terms of the Sheffer Stroke, prove a Sheffer stroke form +% of modularity. + +% Refs : [MRV03] McCune et al. (2003), Sheffer Stroke Bases for Ortholatt +% Source : [MRV03] +% Names : MOL-23C-modularity [MRV03] + +% Status : Open +% Rating : 1.00 v2.6.0 +% Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) +% Number of atoms : 2 ( 2 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 4 ( 3 constant; 0-2 arity) +% Number of variables : 4 ( 1 singleton) +% Maximal term depth : 7 ( 4 average) +% SPC : CNF_OPN_RFO_PEQ_UEQ + +% Comments : +%-------------------------------------------------------------------------- +%----Single axiom MOL-23C +cnf(mol_23C,axiom, + ( f(f(f(B,f(A,B)),B),f(A,f(C,f(f(A,B),f(f(C,C),D))))) = A )). + +%----Denial of Sheffer stroke modularity +cnf(modularity,negated_conjecture, + ( f(a,f(b,f(a,f(c,c)))) != f(a,f(c,f(a,f(b,b)))) )). + +cnf(bonus, axiom, f(A,B)=f(B,A)). + +%-------------------------------------------------------------------------- diff --git a/tests/REL038-1.p b/tests/REL038-1.p new file mode 100644 --- /dev/null +++ b/tests/REL038-1.p @@ -0,0 +1,14 @@ +cnf(maddux1_join_commutativity_1, axiom, join(A, B)=join(B, A)). +cnf(maddux2_join_associativity_2, axiom, join(A, join(B, C))=join(join(A, B), C)). +cnf(maddux3_a_kind_of_de_Morgan_3, axiom, A=join(complement(join(complement(A), complement(B))), complement(join(complement(A), B)))). +cnf(maddux4_definiton_of_meet_4, axiom, meet(A, B)=complement(join(complement(A), complement(B)))). +cnf(composition_associativity_5, axiom, composition(A, composition(B, C))=composition(composition(A, B), C)). +cnf(composition_identity_6, axiom, composition(A, one)=A). +cnf(composition_distributivity_7, axiom, composition(join(A, B), C)=join(composition(A, C), composition(B, C))). +cnf(converse_idempotence_8, axiom, converse(converse(A))=A). +cnf(converse_additivity_9, axiom, converse(join(A, B))=join(converse(A), converse(B))). +cnf(converse_multiplicativity_10, axiom, converse(composition(A, B))=composition(converse(B), converse(A))). +cnf(converse_cancellativity_11, axiom, join(composition(converse(A), complement(composition(A, B))), complement(B))=complement(B)). +cnf(def_top_12, axiom, top=join(A, complement(A))). +cnf(def_zero_13, axiom, zero=meet(A, complement(A))). +cnf(goals_14, negated_conjecture, join(meet(composition(sk1, sk2), sk3), meet(composition(sk1, meet(sk2, composition(converse(sk1), sk3))), sk3))!=meet(composition(sk1, meet(sk2, composition(converse(sk1), sk3))), sk3)). diff --git a/tests/RNG035-7.p b/tests/RNG035-7.p new file mode 100644 --- /dev/null +++ b/tests/RNG035-7.p @@ -0,0 +1,12 @@ +cnf(left_additive_identity, axiom, add(additive_identity, X)=X). +cnf(right_additive_identity, axiom, add(X, additive_identity)=X). +cnf(left_additive_inverse, axiom, add(additive_inverse(X), X)=additive_identity). +cnf(right_additive_inverse, axiom, add(X, additive_inverse(X))=additive_identity). +cnf(associativity_for_addition, axiom, add(X, add(Y, Z))=add(add(X, Y), Z)). +cnf(commutativity_for_addition, axiom, add(X, Y)=add(Y, X)). +cnf(associativity_for_multiplication, axiom, multiply(X, multiply(Y, Z))=multiply(multiply(X, Y), Z)). +cnf(distribute1, axiom, multiply(X, add(Y, Z))=add(multiply(X, Y), multiply(X, Z))). +cnf(distribute2, axiom, multiply(add(X, Y), Z)=add(multiply(X, Z), multiply(Y, Z))). +cnf(x_fourthed_is_x, hypothesis, multiply(X, multiply(X, multiply(X, X)))=X). +cnf(a_times_b_is_c, negated_conjecture, multiply(a, b)=c). +cnf(prove_commutativity, negated_conjecture, multiply(b, a)!=c). diff --git a/tests/ROB027-1.p b/tests/ROB027-1.p --- a/tests/ROB027-1.p +++ b/tests/ROB027-1.p @@ -44,13 +44,7 @@ ( negate(negate(c)) = c )). cnf(prove_huntingtons_axiom,negated_conjecture, - goal_lhs != b). - -cnf(anb, axiom, goal_anb = add(a, negate(b))). -cnf(nanb, axiom, goal_nanb = add(negate(a), negate(b))). -cnf(n_nanb, axiom, goal_n_nanb = negate(goal_nanb)). -cnf(n_anb, axiom, goal_n_anb = negate(goal_anb)). -cnf(lhs, axiom, goal_lhs = add(goal_n_anb, goal_n_nanb)). + add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b). %-------------------------------------------------------------------------- %----Definition of g diff --git a/tests/append-rev.p b/tests/append-rev.p --- a/tests/append-rev.p +++ b/tests/append-rev.p @@ -1,4 +1,4 @@ cnf(rev_rev, axiom, rev(rev(X)) = X). -cnf(app_assoc, axiom, '++'(X,'++'(Y,Z)) = '++'('++'(X,Y),Z)). -cnf(rev_app, axiom, '++'(rev(X),rev(Y)) = rev('++'(Y,X))). -cnf(conjecture, negated_conjecture, '++'(a,rev(b)) != rev('++'(b, rev(a)))). +cnf(app_assoc, axiom, X ++ (Y ++ Z) = (X ++ Y) ++ Z). +cnf(rev_app, axiom, rev(X) ++ rev(Y) = rev(Y ++ X)). +cnf(conjecture, conjecture, a ++ rev(b) = rev(b ++ rev(a))). diff --git a/tests/blah.p b/tests/blah.p new file mode 100644 --- /dev/null +++ b/tests/blah.p @@ -0,0 +1,5 @@ +cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(plus_zero, axiom, '+'('0', X) = X). +cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0'). +cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). diff --git a/tests/db-goal.p b/tests/db-goal.p deleted file mode 100644 --- a/tests/db-goal.p +++ /dev/null @@ -1,22 +0,0 @@ -% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf -% appendix b. theorem 3.4, clause 8. -cnf(a, axiom, '^'(X, Y) = '^'(Y, X)). -cnf(a, axiom, '^'(X, '^'(Y, Z)) = '^'(Y, '^'(X, Z))). -cnf(a, axiom, '^'('^'(X, Y), Z) = '^'(X, '^'(Y, Z))). -cnf(a, axiom, v(X, Y) = v(Y, X)). -cnf(a, axiom, v(X, v(Y, Z)) = v(Y, v(X, Z))). -cnf(a, axiom, v(v(X, Y), Z) = v(X, v(Y, Z))). -cnf(a, axiom, v(X, '^'(X, Y)) = X). -cnf(a, axiom, '^'(X, v(X, Y)) = X). -cnf(a, axiom, upme(X,Y,Z) = '^'(X, v(Y, Z))). -cnf(a, axiom, lome(X,Y,Z) = v('^'(X, Y), '^'(X, Z))). -cnf(a, axiom, upjo(X,Y,Z) = '^'(v(X, Y), v(X, Z))). -cnf(a, axiom, lojo(X,Y,Z) = v(X, '^'(Y, Z))). -cnf(a, axiom, v(upme('^'(a, X1),Y1,Z1), '^'(Y1, Z1)) = '^'(v('^'('^'(a, X1), Y1), Z1), v('^'('^'(a, X1), Z1), Y1))). -cnf(a, axiom, upme(X,Y,Z) = v(upme(X,Y,'^'(a, Z)), upme(X,Z,'^'(a, Y)))). -cnf(c1, axiom, c1 = upme(a,x2,y2)). -cnf(c2, axiom, c2 = upme(a,x2,z2)). -cnf(c3, axiom, c3 = upme(x2,y2,z2)). -cnf(c4, axiom, c4 = lome(x2,y2,z2)). -fof(a, conjecture, c1 = c2 => c3 = c4). -%fof(a, conjecture, (upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2))). diff --git a/tests/db.p b/tests/db.p --- a/tests/db.p +++ b/tests/db.p @@ -1,17 +1,28 @@ % http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf % appendix b. theorem 3.4, clause 8. -cnf(a, axiom, '^'(X, Y) = '^'(Y, X)). -cnf(a, axiom, '^'(X, '^'(Y, Z)) = '^'(Y, '^'(X, Z))). -cnf(a, axiom, '^'('^'(X, Y), Z) = '^'(X, '^'(Y, Z))). -cnf(a, axiom, v(X, Y) = v(Y, X)). -cnf(a, axiom, v(X, v(Y, Z)) = v(Y, v(X, Z))). -cnf(a, axiom, v(v(X, Y), Z) = v(X, v(Y, Z))). -cnf(a, axiom, v(X, '^'(X, Y)) = X). -cnf(a, axiom, '^'(X, v(X, Y)) = X). -cnf(a, axiom, upme(X,Y,Z) = '^'(X, v(Y, Z))). -cnf(a, axiom, lome(X,Y,Z) = v('^'(X, Y), '^'(X, Z))). -cnf(a, axiom, upjo(X,Y,Z) = '^'(v(X, Y), v(X, Z))). -cnf(a, axiom, lojo(X,Y,Z) = v(X, '^'(Y, Z))). -cnf(a, axiom, v(upme('^'(a, X1),Y1,Z1), '^'(Y1, Z1)) = '^'(v('^'('^'(a, X1), Y1), Z1), v('^'('^'(a, X1), Z1), Y1))). -cnf(a, axiom, upme(X,Y,Z) = v(upme(X,Y,'^'(a, Z)), upme(X,Z,'^'(a, Y)))). -fof(a, conjecture, (upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2))). +cnf(commutativity, axiom, + X ∧ Y = Y ∧ X). +cnf(associativity, axiom, + X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z). +cnf(commutativity, axiom, + X ∨ Y = Y ∨ X). +cnf(associativity, axiom, + X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z). +cnf(absorption, axiom, + X ∨ (X ∧ Y) = X). +cnf(absorption, axiom, + X ∧ (X ∨ Y) = X). +cnf('definition of upme', axiom, + upme(X,Y,Z) = X ∧ (Y ∨ Z)). +cnf('definition of lome', axiom, + lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)). +%cnf('definition of upjo', axiom, +% upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)). +%cnf('definition of lojo' axiom, +% lojo(X,Y,Z) = X ∨ (Y ∧ Z)). +cnf('upme property 1', axiom, + upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)). +cnf('upme property 2', axiom, + upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)). +fof(conjecture, conjecture, + upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2)). diff --git a/tests/db2.p b/tests/db2.p new file mode 100644 --- /dev/null +++ b/tests/db2.p @@ -0,0 +1,29 @@ +% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf +% appendix b. theorem 3.4, clause 8. +cnf(commutativity, axiom, + X ∧ Y = Y ∧ X). +cnf(associativity, axiom, + X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z). +cnf(commutativity, axiom, + X ∨ Y = Y ∨ X). +cnf(associativity, axiom, + X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z). +cnf(absorption, axiom, + X ∨ (X ∧ Y) = X). +cnf(absorption, axiom, + X ∧ (X ∨ Y) = X). +cnf('definition of upme', axiom, + upme(X,Y,Z) = X ∧ (Y ∨ Z)). +cnf('definition of lome', axiom, + lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)). +cnf('definition of upjo', axiom, + upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)). +cnf('definition of lojo', axiom, + lojo(X,Y,Z) = X ∨ (Y ∧ Z)). +cnf('upme property 1', axiom, + ((a ∧ X1) ∧ (Y1 ∨ Z1)) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)). +cnf('upme property 2', axiom, + X ∧ (Y ∨ Z) = (X ∧ (Y ∨ (a ∧ Z))) ∨ (X ∧ (Z ∨ (a ∧ Y)))). +fof(conjecture, conjecture, + a ∧ (x2 ∨ y2) = a ∧ (x2 ∨ z2) => + x2 ∧ (y2 ∨ z2) = (x2 ∧ y2) ∨ (x2 ∧ z2)). diff --git a/tests/deriv.p b/tests/deriv.p --- a/tests/deriv.p +++ b/tests/deriv.p @@ -1,39 +1,37 @@ % Axioms about arithmetic. cnf('commutativity of +', axiom, - '+'(X, Y) = '+'(Y, X)). + X + Y = Y + X). cnf('associativity of +', axiom, - '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). + X + (Y + Z) = (X + Y) + Z). cnf('commutativity of *', axiom, - '*'(X, Y) = '*'(Y, X)). + X * Y = Y * X). cnf('associativity of *', axiom, - '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). + X * (Y * Z) = (X * Y) * Z). cnf('plus 0', axiom, - '+'('0', X) = X). + '0' + X = X). cnf('times 0', axiom, - '*'('0', X) = '0'). + '0' * X = '0'). cnf('times 1', axiom, - '*'('1', X) = X). + '1' * X = X). cnf('distributivity', axiom, - '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). + X * (Y + Z) = (X * Y) + (X * Z)). cnf('minus', axiom, - '+'(X, '-'(X)) = '0'). - + X + -X = '0'). cnf('derivative of 0', axiom, - d('0') = '0'). + d('0') = '0'). cnf('derivative of 1', axiom, - d('1') = '0'). + d('1') = '0'). cnf('derivative of x', axiom, - d(x) = '1'). + d(x) = '1'). cnf('derivative of +', axiom, - d('+'(T,U)) = '+'(d(T), d(U))). + d(T+U) = d(T) + d(U)). cnf('derivative of *', axiom, - d('*'(T, U)) = '+'('*'(T, d(U)), '*'(U, d(T)))). + d(T*U) = (T*d(U)) + (U*d(T))). cnf('derivative of sin', axiom, - d(sin(T)) = '*'(cos(T), d(T))). + d(sin(T)) = cos(T) * d(T)). cnf('derivative of cos', axiom, - d(cos(T)) = '-'('*'(sin(T), d(T)))). + d(cos(T)) = -(sin(T)*d(T))). fof(goal, conjecture, - ?[T]: d(T) = '*'(x, cos(x))). - + ?[T]: d(T) = x*cos(x)). diff --git a/tests/diff.p b/tests/diff.p --- a/tests/diff.p +++ b/tests/diff.p @@ -1,4 +1,8 @@ -cnf('x\\(y\\x)=x', axiom, '\\'(X, '\\'(Y, X)) = X). -cnf('x\\(x\\y)=y\\(y\\x)', axiom, '\\'(X, '\\'(X, Y)) = '\\'(Y, '\\'(Y, X))). -cnf('(x\\y)\\z=(x\\z)\\(y\\z)', axiom, '\\'('\\'(X, Y), Z) = '\\'('\\'(X, Z), '\\'(Y, Z))). -cnf(conjecture, negated_conjecture, '\\'('\\'(a, c), b) != '\\'('\\'(a, b), c)). +cnf('x\\(y\\x)=x', axiom, + X \ (Y \ X) = X). +cnf('x\\(x\\y)=y\\(y\\x)', axiom, + X \ (X \ Y) = Y \ (Y \ X)). +cnf('(x\\y)\\z=(x\\z)\\(y\\z)', axiom, + (X \ Y) \ Z = (X \ Z) \ (Y \ Z)). +cnf(conjecture, conjecture, + (a \ c) \ b = (a \ b) \ c). diff --git a/tests/factor.p b/tests/factor.p new file mode 100644 --- /dev/null +++ b/tests/factor.p @@ -0,0 +1,50 @@ +% Axioms about arithmetic. + +cnf('commutativity of +', axiom, + X + Y = Y + X). +cnf('associativity of +', axiom, + X + (Y + Z) = (X + Y) + Z). +cnf('commutativity of *', axiom, + X * Y = Y * X). +cnf('associativity of *', axiom, + X * (Y * Z) = (X * Y) * Z). +cnf('plus 0', axiom, + '0' + X = X). +cnf('times 0', axiom, + '0' * X = '0'). +cnf('times 1', axiom, + '1' * X = X). +cnf('distributivity', axiom, + X * (Y + Z) = (X * Y) + (X * Z)). +cnf('minus', axiom, + X + -X = '0'). + +tff(square, type, '_²' : $i > $i). +tff(cube, type, '_³' : $i > $i). +cnf(square, axiom, X² = X*X). +cnf(cube, axiom, X³ = X*(X*X)). +%cnf(two, axiom, two = '1'+'1'). +%cnf(three, axiom, three = '1'+two). +%cnf(four, axiom, four = '1'+three). +%cnf(five, axiom, five = '1'+four). +%cnf(six, axiom, six = '1'+five). +%cnf(seven, axiom, seven = '1'+six). +%cnf(eight, axiom, eight = '1'+seven). +%cnf(nine, axiom, nine = '1'+eight). +%cnf(minus_six, axiom, minus_four = -four). +%cnf(minus_six, axiom, minus_six = -six). + +%fof(factoring, conjecture, +% ?[A,B,C]: ![X]: +% X³ + ((minus_six*(X²)) + ((nine*X) + minus_four)) = ((X + +% -'1')*((X + -'1') * (X + -four)))). + +%cnf(a, conjecture, (-x)*y = -(y*x)). + +fof(factoring, conjecture, + ?[A,B,C]: ![X]: + X³ + + (-(('1'+('1'+('1'+('1'+('1'+'1')))))*(X²)) + + ((('1'+('1'+('1'+('1'+('1'+('1'+('1'+('1'+'1'))))))))*X) + + -('1'+('1'+('1'+'1'))))) = + (X + -A)*((X + -B)*(X + -C))). diff --git a/tests/fol.p b/tests/fol.p deleted file mode 100644 --- a/tests/fol.p +++ /dev/null @@ -1,16 +0,0 @@ -cnf(ifeq_axiom, axiom, ifeq(A, A, B, C)=B). -cnf(ifeq_axiom, axiom, ifeq(X2, X2, U2, V2)=U2). -cnf(ifeq_axiom, axiom, ifeq(X2, Y2, U2, U2)=U2). -cnf(ifeq_axiom, axiom, ifeq(X2, Y2, X2, Y2)=Y2). -cnf(ifeq_axiom, axiom, - ifeq(ifeq(U2, V2, A4, B4), ifeq(U2, V2, A3, B3), - ifeq(U2, V2, A, B), ifeq(U2, V2, A2, B2))=ifeq(U2, V2, - ifeq(A4, A3, A, A2), - ifeq(B4, B3, B, B2))). -cnf(ifeq_axiom, axiom, - ifeq(X2, Y2, ifeq(X2, Y2, U2, V2), - ifeq(X2, Y2, S2, T2))=ifeq(X2, Y2, U2, T2)). -cnf(a, axiom, ifeq(p, true, q, true)=q). -cnf(a, negated_conjecture, ifeq(q, true, a, b)=b). -cnf(a_1, negated_conjecture, ifeq(p, true, a, b)=b). -cnf(goal, negated_conjecture, a!=b). diff --git a/tests/group.p b/tests/group.p --- a/tests/group.p +++ b/tests/group.p @@ -1,16 +1,14 @@ -%fof(identity, axiom, -% ![X]: f(X, e) = X). -%fof(right_inverse, axiom, -% ![X]: f(X, i(X)) = e). -fof(associativity, axiom, - ![X, Y, Z]: f(X, f(Y, Z)) = f(f(X, Y), Z)). -fof(left_inverse, axiom, - ![X]: f(i(X),X) = e). -fof(left_identity, axiom, - ![X]: f(e, X) = X). -cnf(a, axiom, a != b). - -%fof(inverse_distrib, axiom, -% ![X,Y]: f(i(X),i(Y)) = i(f(X,Y))). -%fof(commutativity, conjecture, -% ![X,Y]: f(X,Y) = f(Y,X)). +cnf(associativity, axiom, + X + (Y + Z) = (X + Y) + Z). +cnf(plus_zero, axiom, + '0' + X = X). +cnf(plus_zero, axiom, + X + '0' = X). +cnf(minus_left, axiom, + (-X) + X = '0'). +cnf(minus_right, axiom, + X + (-X) = '0'). +cnf(assumption, assumption, + a + b = a). +cnf(goal, conjecture, + b = '0'). diff --git a/tests/haken.p b/tests/haken.p new file mode 100644 --- /dev/null +++ b/tests/haken.p @@ -0,0 +1,170 @@ +cnf(a, conjecture, a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & +a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 & a10 = a11 & a11 = a12 & a12 = +a13 & a13 = a14 & a14 = a15 & a15 = a16 & a16 = a17 & a17 = a18 & a18 += a19 & a19 = a20 & a20 = a21 & a20 = a22 & a21 = a23 & a23 = a24 & +a24 = a25 & a25 = a26 & a26 = a27 & a27 = a28 & a28 = a29 & a29 = a30 +& a30 = a31 & a31 = a32 & a32 = a33 & a33 = a34 & a34 = a35 & a35 = +a36 & a36 = a37 & a37 = a38 & a38 = a39 & a39 = a40 & a40 = a41 & a41 += a42 & a42 = a43 & a43 = a44 & a44 = a45 & a45 = a46 & a46 = a47 & +a47 = a48 & a48 = a49 & a49 = a50 & a50 = a51 & a51 = a52 & a52 = a53 +& a53 = a54 & a54 = a55 & a55 = a56 & a56 = a57 & a57 = a58 & a58 = +a59 & a59 = a60 & a60 = a61 & a61 = a62 & a62 = a63 & a63 = a64 & a64 += a65 & a65 = a66 & a66 = a67 & a67 = a68 & a68 = a69 & a69 = a70 & +a70 = a71 & a71 = a72 & a72 = a73 & a73 = a74 & a74 = a75 & a75 = a76 +& a76 = a77 & a77 = a78 & a78 = a79 & a79 = a80 & a80 = a81 & a81 = +a82 & a82 = a83 & a83 = a84 & a84 = a85 & a85 = a86 & a86 = a87 & a87 += a88 & a88 = a89 & a89 = a90 & a90 = a91 & a91 = a92 & a92 = a93 & +a93 = a94 & a94 = a95 & a95 = a96 & a96 = a97 & a97 = a98 & a98 = a99 +& a99 = a100 & a100 = a101 & a101 = a102 & a102 = a103 & a103 = a104 & +a104 = a105 & a105 = a106 & a106 = a107 & a107 = a108 & a108 = a109 & +a109 = a110 & a110 = a111 & a111 = a112 & a112 = a113 & a113 = a114 & +a114 = a115 & a115 = a116 & a116 = a117 & a117 = a118 & a118 = a119 & +a119 = a120 & a120 = a121 & a121 = a122 & a122 = a123 & a123 = a124 & +a124 = a125 & a125 = a126 & a126 = a127 & a127 = a128 & a128 = a129 & +a129 = a130 & a130 = a131 & a131 = a132 & a132 = a133 & a133 = a134 & +a134 = a135 & a135 = a136 & a136 = a137 & a137 = a138 & a138 = a139 & +a139 = a140 & a140 = a141). +cnf(a, axiom, '*'(X, X) = X). +cnf(a, axiom, '*'('*'(X,Y),Y) = X). +cnf(a, axiom, '*'('*'(X,Y),Z) = '*'('*'(X, Z), '*'(Y, Z))). +cnf(a, axiom, a2 = '*'(a1, a42)). +cnf(a, axiom, a3 = '*'(a2, a41)). +cnf(a, axiom, a4 = '*'(a3, a14)). +cnf(a, axiom, a5 = '*'(a4, a39)). +cnf(a, axiom, a6 = '*'(a5, a136)). +cnf(a, axiom, a7 = '*'(a6, a52)). +cnf(a, axiom, a8 = '*'(a7, a17)). +cnf(a, axiom, a9 = '*'(a8, a56)). +cnf(a, axiom, a10 = '*'(a9, a134)). +cnf(a, axiom, a11 = '*'(a10, a37)). +cnf(a, axiom, a12 = '*'(a11, a21)). +cnf(a, axiom, a13 = '*'(a12, a23)). +cnf(a, axiom, a14 = '*'(a13, a32)). +cnf(a, axiom, a15 = '*'(a14, a53)). +cnf(a, axiom, a16 = '*'(a15, a136)). +cnf(a, axiom, a17 = '*'(a16, a29)). +cnf(a, axiom, a18 = '*'(a17, a133)). +cnf(a, axiom, a19 = '*'(a18, a58)). +cnf(a, axiom, a20 = '*'(a19, a26)). +cnf(a, axiom, a21 = '*'(a20, a35)). +cnf(a, axiom, a22 = '*'(a21, a141)). +cnf(a, axiom, a23 = '*'(a22, a45)). +cnf(a, axiom, a24 = '*'(a23, a35)). +cnf(a, axiom, a25 = '*'(a24, a49)). +cnf(a, axiom, a26 = '*'(a25, a138)). +cnf(a, axiom, a27 = '*'(a26, a8)). +cnf(a, axiom, a28 = '*'(a27, a37)). +cnf(a, axiom, a29 = '*'(a28, a17)). +cnf(a, axiom, a30 = '*'(a29, a14)). +cnf(a, axiom, a31 = '*'(a30, a5)). +cnf(a, axiom, a32 = '*'(a31, a39)). +cnf(a, axiom, a33 = '*'(a32, a13)). +cnf(a, axiom, a34 = '*'(a33, a131)). +cnf(a, axiom, a35 = '*'(a34, a60)). +cnf(a, axiom, a36 = '*'(a35, a139)). +cnf(a, axiom, a37 = '*'(a36, a47)). +cnf(a, axiom, a38 = '*'(a37, a17)). +cnf(a, axiom, a39 = '*'(a38, a7)). +cnf(a, axiom, a40 = '*'(a39, a4)). +cnf(a, axiom, a41 = '*'(a40, a14)). +cnf(a, axiom, a42 = '*'(a41, a2)). +cnf(a, axiom, a43 = '*'(a42, a62)). +cnf(a, axiom, a44 = '*'(a43, a128)). +cnf(a, axiom, a45 = '*'(a44, a23)). +cnf(a, axiom, a46 = '*'(a45, a141)). +cnf(a, axiom, a47 = '*'(a46, a11)). +cnf(a, axiom, a48 = '*'(a47, a20)). +cnf(a, axiom, a49 = '*'(a48, a138)). +cnf(a, axiom, a50 = '*'(a49, a131)). +cnf(a, axiom, a51 = '*'(a50, a59)). +cnf(a, axiom, a52 = '*'(a51, a39)). +cnf(a, axiom, a53 = '*'(a52, a136)). +cnf(a, axiom, a54 = '*'(a53, a29)). +cnf(a, axiom, a55 = '*'(a54, a135)). +cnf(a, axiom, a56 = '*'(a55, a37)). +cnf(a, axiom, a57 = '*'(a56, a134)). +cnf(a, axiom, a58 = '*'(a57, a26)). +cnf(a, axiom, a59 = '*'(a58, a138)). +cnf(a, axiom, a60 = '*'(a59, a131)). +cnf(a, axiom, a61 = '*'(a60, a13)). +cnf(a, axiom, a62 = '*'(a61, a1)). +cnf(a, axiom, a63 = '*'(a62, a96)). +cnf(a, axiom, a64 = '*'(a63, a127)). +cnf(a, axiom, a65 = '*'(a64, a41)). +cnf(a, axiom, a66 = '*'(a65, a2)). +cnf(a, axiom, a67 = '*'(a66, a92)). +cnf(a, axiom, a68 = '*'(a67, a98)). +cnf(a, axiom, a69 = '*'(a68, a32)). +cnf(a, axiom, a70 = '*'(a69, a13)). +cnf(a, axiom, a71 = '*'(a70, a118)). +cnf(a, axiom, a72 = '*'(a71, a109)). +cnf(a, axiom, a73 = '*'(a72, a82)). +cnf(a, axiom, a74 = '*'(a73, a32)). +cnf(a, axiom, a75 = '*'(a74, a14)). +cnf(a, axiom, a76 = '*'(a75, a68)). +cnf(a, axiom, a77 = '*'(a76, a114)). +cnf(a, axiom, a78 = '*'(a77, a13)). +cnf(a, axiom, a79 = '*'(a78, a33)). +cnf(a, axiom, a80 = '*'(a79, a119)). +cnf(a, axiom, a81 = '*'(a80, a70)). +cnf(a, axiom, a82 = '*'(a81, a109)). +cnf(a, axiom, a83 = '*'(a82, a118)). +cnf(a, axiom, a84 = '*'(a83, a39)). +cnf(a, axiom, a85 = '*'(a84, a5)). +cnf(a, axiom, a86 = '*'(a85, a30)). +cnf(a, axiom, a87 = '*'(a86, a104)). +cnf(a, axiom, a88 = '*'(a87, a4)). +cnf(a, axiom, a89 = '*'(a88, a14)). +cnf(a, axiom, a90 = '*'(a89, a41)). +cnf(a, axiom, a91 = '*'(a90, a100)). +cnf(a, axiom, a92 = '*'(a91, a124)). +cnf(a, axiom, a93 = '*'(a92, a2)). +cnf(a, axiom, a94 = '*'(a93, a41)). +cnf(a, axiom, a95 = '*'(a94, a127)). +cnf(a, axiom, a96 = '*'(a95, a64)). +cnf(a, axiom, a97 = '*'(a96, a42)). +cnf(a, axiom, a98 = '*'(a97, a1)). +cnf(a, axiom, a99 = '*'(a98, a92)). +cnf(a, axiom, a100 = '*'(a99, a124)). +cnf(a, axiom, a101 = '*'(a100, a14)). +cnf(a, axiom, a102 = '*'(a101, a40)). +cnf(a, axiom, a103 = '*'(a102, a4)). +cnf(a, axiom, a104 = '*'(a103, a87)). +cnf(a, axiom, a105 = '*'(a104, a30)). +cnf(a, axiom, a106 = '*'(a105, a5)). +cnf(a, axiom, a107 = '*'(a106, a84)). +cnf(a, axiom, a108 = '*'(a107, a39)). +cnf(a, axiom, a109 = '*'(a108, a118)). +cnf(a, axiom, a110 = '*'(a109, a70)). +cnf(a, axiom, a111 = '*'(a110, a119)). +cnf(a, axiom, a112 = '*'(a111, a79)). +cnf(a, axiom, a113 = '*'(a112, a33)). +cnf(a, axiom, a114 = '*'(a113, a13)). +cnf(a, axiom, a115 = '*'(a114, a68)). +cnf(a, axiom, a116 = '*'(a115, a14)). +cnf(a, axiom, a117 = '*'(a116, a74)). +cnf(a, axiom, a118 = '*'(a117, a32)). +cnf(a, axiom, a119 = '*'(a118, a70)). +cnf(a, axiom, a120 = '*'(a119, a13)). +cnf(a, axiom, a121 = '*'(a120, a32)). +cnf(a, axiom, a122 = '*'(a121, a68)). +cnf(a, axiom, a123 = '*'(a122, a115)). +cnf(a, axiom, a124 = '*'(a123, a75)). +cnf(a, axiom, a125 = '*'(a124, a2)). +cnf(a, axiom, a126 = '*'(a125, a65)). +cnf(a, axiom, a127 = '*'(a126, a41)). +cnf(a, axiom, a128 = '*'(a127, a96)). +cnf(a, axiom, a129 = '*'(a128, a62)). +cnf(a, axiom, a130 = '*'(a129, a1)). +cnf(a, axiom, a131 = '*'(a130, a13)). +cnf(a, axiom, a132 = '*'(a131, a138)). +cnf(a, axiom, a133 = '*'(a132, a58)). +cnf(a, axiom, a134 = '*'(a133, a26)). +cnf(a, axiom, a135 = '*'(a134, a37)). +cnf(a, axiom, a136 = '*'(a135, a29)). +cnf(a, axiom, a137 = '*'(a136, a39)). +cnf(a, axiom, a138 = '*'(a137, a51)). +cnf(a, axiom, a139 = '*'(a138, a20)). +cnf(a, axiom, a140 = '*'(a139, a47)). +cnf(a, axiom, a141 = '*'(a140, a11)). +cnf(a, axiom, a1 = '*'(a141, a23)). diff --git a/tests/lat.p b/tests/lat.p deleted file mode 100644 --- a/tests/lat.p +++ /dev/null @@ -1,16 +0,0 @@ -cnf(idempotence_of_meet, axiom, meet(X, X)=X). -cnf(idempotence_of_join, axiom, join(X, X)=X). -cnf(absorption1, axiom, meet(X, join(X, Y))=X). -cnf(absorption2, axiom, join(X, meet(X, Y))=X). -cnf(commutativity_of_meet, axiom, meet(X, Y)=meet(Y, X)). -cnf(commutativity_of_join, axiom, join(X, Y)=join(Y, X)). -cnf(associativity_of_meet, axiom, - meet(meet(X, Y), Z)=meet(X, meet(Y, Z))). -cnf(associativity_of_join, axiom, - join(join(X, Y), Z)=join(X, join(Y, Z))). -cnf(equation_H34, axiom, - meet(X, join(Y, meet(Z, U)))=meet(X, - join(Y, meet(Z, join(Y, meet(U, join(Y, Z))))))). -cnf(prove_H28, negated_conjecture, - meet(a, join(b, meet(a, meet(c, d))))!=meet(a, - join(b, meet(c, meet(d, join(a, meet(b, d))))))). diff --git a/tests/lcl.p b/tests/lcl.p deleted file mode 100644 --- a/tests/lcl.p +++ /dev/null @@ -1,7 +0,0 @@ -cnf(wajsberg_1, axiom, implies(truth, X)=X). -cnf(wajsberg_3, axiom, - implies(implies(X, Y), Y)=implies(implies(Y, X), X)). -cnf(wajsberg_4, axiom, - implies(implies(not(X), not(Y)), implies(Y, X))=truth). -cnf(lemma_antecedent, axiom, implies(X, Y)=implies(Y, X)). -cnf(prove_wajsberg_lemma, negated_conjecture, x!=y). diff --git a/tests/loop-ascii.p b/tests/loop-ascii.p new file mode 100644 --- /dev/null +++ b/tests/loop-ascii.p @@ -0,0 +1,6 @@ +cnf(mult_ld, axiom, mult(X, back(X, Y)) = Y). +cnf(ld_mult, axiom, back(X, mult(X, Y)) = Y). +cnf(mult_rd, axiom, mult(slash(X, Y), Y) = X). +cnf(rd_mult, axiom, slash(mult(X, Y), Y) = X). +cnf(moufang, axiom, mult(X, mult(Y, mult(X, Z))) = mult(mult(mult(X, Y), X), Z)). +cnf(conjecture, conjecture, back(a, a) = slash(a, a)). diff --git a/tests/loop.p b/tests/loop.p --- a/tests/loop.p +++ b/tests/loop.p @@ -1,6 +1,6 @@ -cnf(mult_ld, axiom, '*'(X, '^'(X, Y)) = Y). -cnf(ld_mult, axiom, '^'(X, '*'(X, Y)) = Y). -cnf(mult_rd, axiom, '*'('/'(X, Y), Y) = X). -cnf(rd_mult, axiom, '/'('*'(X, Y), Y) = X). -cnf(moufang, axiom, '*'(X, '*'(Y, '*'(X, Z))) = '*'('*'('*'(X, Y), X), Z)). -cnf(conjecture, negated_conjecture, '^'(a,a) != '/'(a,a)). +cnf(mult_ld, axiom, X * (X \ Y) = Y). +cnf(ld_mult, axiom, X \ (X * Y) = Y). +cnf(mult_rd, axiom, (X / Y) * Y = X). +cnf(rd_mult, axiom, (X * Y) / Y = X). +cnf(moufang, axiom, X * (Y * (X * Z)) = ((X * Y) * X) * Z). +cnf(conjecture, conjecture, a \ a = a / a). diff --git a/tests/loop2.p b/tests/loop2.p --- a/tests/loop2.p +++ b/tests/loop2.p @@ -1,6 +1,6 @@ -cnf('*-\\', axiom, '*'(X, '\\'(X, Y)) = Y). -cnf('\\-*', axiom, '\\'(X, '*'(X, Y)) = Y). -cnf('*-/', axiom, '*'('/'(X, Y), Y) = X). -cnf('/-*', axiom, '/'('*'(X, Y), Y) = X). -cnf(moufang, axiom, '*'(X, '*'(Y, '*'(X, Z))) = '*'('*'('*'(X, Y), X), Z)). -cnf(conjecture, negated_conjecture, '*'(a,'/'(b,b)) != a). +cnf('*-\\', axiom, X * (X \ Y) = Y). +cnf('\\-*', axiom, X \ (X * Y) = Y). +cnf('*-/', axiom, (X / Y) * Y = X). +cnf('/-*', axiom, (X * Y) / Y = X). +cnf(moufang, axiom, X * (Y * (X * Z)) = ((X * Y) * X) * Z). +cnf(conjecture, conjecture, a * (b / b) = a). diff --git a/tests/minus.p b/tests/minus.p --- a/tests/minus.p +++ b/tests/minus.p @@ -1,12 +1,10 @@ cnf(plus_zero, axiom, - '+'('0', X) = X). + '0' + X = X). cnf(plus_zero, axiom, - '+'(X, '0') = X). + X + '0' = X). cnf(minus_minus, axiom, - '-'('-'(X)) = X). + - -X = X). cnf(minus_plus, axiom, - '-'('+'(X, Y)) = '+'('-'(X), '-'(Y))). - + -(X + Y) = -X + -Y). cnf(goal, conjecture, - '-'('0') = '0'). - %% ?[Y]: d(Y) = '+'(x, x)). + -'0' = '0'). diff --git a/tests/nand-goal.p b/tests/nand-goal.p deleted file mode 100644 --- a/tests/nand-goal.p +++ /dev/null @@ -1,44 +0,0 @@ -%-------------------------------------------------------------------------- -% File : LAT071-1 : TPTP v6.2.0. Released v2.6.0. -% Domain : Lattice Theory (Orthomodularlattices) -% Problem : Given single axiom OML-21C, prove associativity -% Version : [MRV03] (equality) axioms. -% English : Given a single axiom candidate OML-21C for orthomodular lattices -% (OML) in terms of the Sheffer Stroke, prove a Sheffer stroke form -% of associativity. - -% Refs : [MRV03] McCune et al. (2003), Sheffer Stroke Bases for Ortholatt -% Source : [MRV03] -% Names : OML-21C-associativity [MRV03] - -% Status : Open -% Rating : 1.00 v2.6.0 -% Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) -% Number of atoms : 2 ( 2 equality) -% Maximal clause size : 1 ( 1 average) -% Number of predicates : 1 ( 0 propositional; 2-2 arity) -% Number of functors : 4 ( 3 constant; 0-2 arity) -% Number of variables : 4 ( 2 singleton) -% Maximal term depth : 6 ( 4 average) -% SPC : CNF_UNK_UEQ - -% Comments : -%-------------------------------------------------------------------------- -%----Single axiom OML-21C -cnf(oml_21C,axiom, - ( f(f(B,A),f(f(f(f(B,A),A),f(C,A)),f(f(A,A),D))) = A )). - -cnf(a, axiom, f(z, f(z, z)) = k). -cnf(fbc, axiom, fbc=f(b,c)). -cnf(fba, axiom, fba=f(b,a)). -cnf(fbc2, axiom, fbc2=f(fbc,fbc)). -cnf(fba2, axiom, fba2=f(fba,fba)). -cnf(lhs, axiom, lhs=f(a,fbc2)). -cnf(rhs, axiom, rhs=f(c,fba2)). -cnf(comm, axiom, f(X,Y)=f(Y,X)). - -%----Denial of Sheffer stroke associativity -cnf(associativity,negated_conjecture, - lhs != rhs). - -%-------------------------------------------------------------------------- diff --git a/tests/nand.p b/tests/nand.p deleted file mode 100644 --- a/tests/nand.p +++ /dev/null @@ -1,37 +0,0 @@ -%-------------------------------------------------------------------------- -% File : LAT071-1 : TPTP v6.2.0. Released v2.6.0. -% Domain : Lattice Theory (Orthomodularlattices) -% Problem : Given single axiom OML-21C, prove associativity -% Version : [MRV03] (equality) axioms. -% English : Given a single axiom candidate OML-21C for orthomodular lattices -% (OML) in terms of the Sheffer Stroke, prove a Sheffer stroke form -% of associativity. - -% Refs : [MRV03] McCune et al. (2003), Sheffer Stroke Bases for Ortholatt -% Source : [MRV03] -% Names : OML-21C-associativity [MRV03] - -% Status : Open -% Rating : 1.00 v2.6.0 -% Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) -% Number of atoms : 2 ( 2 equality) -% Maximal clause size : 1 ( 1 average) -% Number of predicates : 1 ( 0 propositional; 2-2 arity) -% Number of functors : 4 ( 3 constant; 0-2 arity) -% Number of variables : 4 ( 2 singleton) -% Maximal term depth : 6 ( 4 average) -% SPC : CNF_UNK_UEQ - -% Comments : -%-------------------------------------------------------------------------- -%----Single axiom OML-21C -cnf(oml_21C,axiom, - ( f(f(B,A),f(f(f(f(B,A),A),f(C,A)),f(f(A,A),D))) = A )). - -cnf(a, axiom, f(z, f(z, z)) = k). - -%----Denial of Sheffer stroke associativity -cnf(associativity,negated_conjecture, - ( f(a,f(f(b,c),f(b,c))) != f(c,f(f(b,a),f(b,a))) )). - -%-------------------------------------------------------------------------- diff --git a/tests/nicomachus.p b/tests/nicomachus.p --- a/tests/nicomachus.p +++ b/tests/nicomachus.p @@ -1,18 +1,36 @@ -cnf(plus_comm, axiom, plus(X, Y) = plus(Y, X)). -cnf(plus_assoc, axiom, plus(X, plus(Y, Z)) = plus(plus(X, Y), Z)). -cnf(times_comm, axiom, times(X, Y) = times(Y, X)). -cnf(times_assoc, axiom, times(X, times(Y, Z)) = times(times(X, Y), Z)). -cnf(plus_zero, axiom, plus(X, zero) = X). -cnf(times_zero, axiom, times(X, zero) = zero). -cnf(times_one, axiom, times(X, one) = X). -cnf(distr, axiom, times(X, plus(Y, Z)) = plus(times(X, Y), times(X, Z))). -cnf(distr, axiom, times(plus(X, Y), Z) = plus(times(X, Z), times(Y, Z))). -cnf(plus_s, axiom, plus(s(X), Y) = s(plus(X, Y))). -cnf(times_s, axiom, times(s(X), Y) = plus(Y, times(X, Y))). -cnf(sum_zero, axiom, sum(zero) = zero). -cnf(sum_s, axiom, sum(s(N)) = plus(s(N), sum(N))). -cnf(cubes_zero, axiom, cubes(zero) = zero). -cnf(cubes_s, axiom, cubes(s(N)) = plus(times(s(N), times(s(N), s(N))), cubes(N))). -cnf(plus_sum, axiom, plus(sum(N), sum(N)) = times(N, s(N))). -cnf(ih, axiom, times(sum(a), sum(a)) = cubes(a)). -cnf(conjecture, negated_conjecture, times(sum(s(a)), sum(s(a))) != cubes(s(a))). +cnf(plus_comm, axiom, + X + Y = Y + X). +cnf(plus_assoc, axiom, + X + (Y + Z) = (X + Y) + Z). +cnf(times_comm, axiom, + X * Y = Y * X). +cnf(times_assoc, axiom, + X * (Y * Z) = (X * Y) * Z). +cnf(plus_zero, axiom, + X + zero = X). +cnf(times_zero, axiom, + X * zero = zero). +cnf(times_one, axiom, + X * one = X). +cnf(distr, axiom, + X * (Y + Z) = (X * Y) + (X * Z)). +cnf(distr, axiom, + (X + Y) * Z = (X * Z) + (Y * Z)). +cnf(plus_s, axiom, + s(X) + Y = s(X+Y)). +cnf(times_s, axiom, + s(X)*Y = Y + (X*Y)). +cnf(sum_zero, axiom, + sum(zero) = zero). +cnf(sum_s, axiom, + sum(s(N)) = s(N) + sum(N)). +cnf(cubes_zero, axiom, + cubes(zero) = zero). +cnf(cubes_s, axiom, + cubes(s(N)) = (s(N) * (s(N) * s(N))) + cubes(N)). +cnf(plus_sum, axiom, + sum(N) + sum(N) = N * s(N)). +cnf(ih, axiom, + sum(a) * sum(a) = cubes(a)). +cnf(conjecture, conjecture, + sum(s(a)) * sum(s(a)) = cubes(s(a))). diff --git a/tests/rel.p b/tests/rel.p new file mode 100644 --- /dev/null +++ b/tests/rel.p @@ -0,0 +1,32 @@ +tff(type, type, '_⁻¹' : $i > $i). +tff(type, type, '_⁻' : $i > $i). + +cnf('commutativity of ∨', axiom, + A ∨ B = B ∨ A). +cnf('associativity of ∨', axiom, + A ∨ (B ∨ C) = (A ∨ B) ∨ C). +cnf('a kind of de Morgan', axiom, + (A⁻ ∨ B⁻)⁻ ∨ (A⁻ ∨ B)⁻ = A). +cnf('definition of ∧', axiom, + A ∧ B = (A⁻ ∨ B⁻)⁻). +cnf('associativity of ;', axiom, + A ; (B ; C) = (A ; B) ; C). +cnf('identity for ;', axiom, + A ; '1' = A). +cnf('distributivity of ; over ∨', axiom, + (A ∨ B) ; C = (A ; C) ∨ (B ; C)). +cnf('involution of ⁻¹', axiom, + A⁻¹ ⁻¹ = A). +cnf('additivity of ⁻¹', axiom, + (A ∨ B)⁻¹ = A⁻¹ ∨ B⁻¹). +cnf('multiplicativity of ⁻¹', axiom, + (A ; B)⁻¹ = B⁻¹ ; A⁻¹). +cnf('cancellativity of ⁻', axiom, + (A⁻¹ ; (A ; B)⁻) ∨ B⁻ = B⁻). +cnf('definition of top', axiom, + top = A ∨ A⁻). +cnf('definition of zero', axiom, + zero = A ∧ A⁻). +cnf(goal, conjecture, + (r1 ; (r2 ∧ r3)) ∨ ((r1 ; r2) ∧ (r1 ; r3)) = + (r1 ; r2) ∧ (r1 ; r3)). diff --git a/tests/rel2.p b/tests/rel2.p new file mode 100644 --- /dev/null +++ b/tests/rel2.p @@ -0,0 +1,32 @@ +tff(type, type, '_⁻¹' : $i > $i). +tff(type, type, '_⁻' : $i > $i). + +cnf('commutativity of ∨', axiom, + A ∨ B = B ∨ A). +cnf('associativity of ∨', axiom, + A ∨ (B ∨ C) = (A ∨ B) ∨ C). +cnf('a kind of de Morgan', axiom, + (A⁻ ∨ B⁻)⁻ ∨ (A⁻ ∨ B)⁻ = A). +cnf('definition of ∧', axiom, + A ∧ B = (A⁻ ∨ B⁻)⁻). +cnf('associativity of ;', axiom, + A ; (B ; C) = (A ; B) ; C). +cnf('identity for ;', axiom, + A ; '1' = A). +cnf('distributivity of ; over ∨', axiom, + (A ∨ B) ; C = (A ; C) ∨ (B ; C)). +cnf('involution of ⁻¹', axiom, + A⁻¹ ⁻¹ = A). +cnf('additivity of ⁻¹', axiom, + (A ∨ B)⁻¹ = A⁻¹ ∨ B⁻¹). +cnf('multiplicativity of ⁻¹', axiom, + (A ; B)⁻¹ = B⁻¹ ; A⁻¹). +cnf('cancellativity of ⁻', axiom, + (A⁻¹ ; (A ; B)⁻) ∨ B⁻ = B⁻). +cnf('definition of top', axiom, + top = A ∨ A⁻). +cnf('definition of zero', axiom, + zero = A ∧ A⁻). +cnf(goal, conjecture, + ((r1 ; r2) ∧ r3) ∨ ((r1; (r2 ∧ (r1⁻¹ ; r3))) ∧ r3) = + (r1 ; (r2 ∧ (r1⁻¹ ; r3))) ∧ r3). diff --git a/tests/ring-goal.p b/tests/ring-goal.p deleted file mode 100644 --- a/tests/ring-goal.p +++ /dev/null @@ -1,11 +0,0 @@ -cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). -cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). -cnf(plus_zero, axiom, '+'('0', X) = X). -cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0'). -cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). -cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). -cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). -cnf(cube, axiom, X = '*'(X, '*'(X, X))). -cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). -cnf(lhs, axiom, lhs = '*'(a, b)). -cnf(rhs, axiom, rhs = '*'(b, a)). diff --git a/tests/ring2-goal.p b/tests/ring2-goal.p deleted file mode 100644 --- a/tests/ring2-goal.p +++ /dev/null @@ -1,12 +0,0 @@ -cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). -cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). -cnf(plus_zero, axiom, '+'('0', X) = X). -cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0'). -cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). -cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). -cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). -cnf(power_six, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, '*'(X, X)))))). -cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). -cnf(lhs, axiom, lhs = '*'(a, b)). -cnf(rhs, axiom, rhs = '*'(b, a)). -cnf(a, axiom, '+'(X, X) = '0'). diff --git a/tests/ring3-goal.p b/tests/ring3-goal.p deleted file mode 100644 --- a/tests/ring3-goal.p +++ /dev/null @@ -1,11 +0,0 @@ -cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). -cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). -cnf(plus_zero, axiom, '+'('0', X) = X). -cnf(plus_neg, axiom, '+'(X, '-'(X)) = '0'). -cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). -cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). -cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). -cnf(power_four, axiom, X = '*'(X, '*'(X, '*'(X, X)))). -cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). -cnf(lhs, axiom, lhs = '*'(a, b)). -cnf(rhs, axiom, rhs = '*'(b, a)). diff --git a/tests/ring4-goal.p b/tests/ring4-goal.p deleted file mode 100644 --- a/tests/ring4-goal.p +++ /dev/null @@ -1,11 +0,0 @@ -cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). -cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). -cnf(plus_zero, axiom, '+'('0', X) = X). -cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0'). -cnf(times_ssoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). -cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). -cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). -cnf(power_five, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, X))))). -cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). -cnf(lhs, axiom, lhs = '*'(a, b)). -cnf(rhs, axiom, rhs = '*'(b, a)). diff --git a/tests/robbins-goal.p b/tests/robbins-goal.p deleted file mode 100644 --- a/tests/robbins-goal.p +++ /dev/null @@ -1,6 +0,0 @@ -cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)). -cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). -cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). -cnf(ma, axiom, '-'(a) = ma). -cnf(mma, axiom, '-'(ma) = mma). -cnf(conjecture, negated_conjecture, mma != a). diff --git a/tests/semigroup2.p b/tests/semigroup2.p deleted file mode 100644 --- a/tests/semigroup2.p +++ /dev/null @@ -1,26 +0,0 @@ -% File : GRP196-1 : TPTP v6.1.0. Released v2.2.0. -% Domain : Group Theory (Semigroups) -% Problem : In semigroups, xyyy=yyyx -> (uy)^9 = u^9v^9. -% Version : [MP96] (equality) axioms. -% English : -% Refs : [McC98] McCune (1998), Email to G. Sutcliffe -% : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq -% : [McC95] McCune (1995), Four Challenge Problems in Equational L -% Source : [McC98] -% Names : CS-3 [MP96] -% : Problem B [McC95] -% Status : Unsatisfiable -% Rating : 1.00 v4.0.1, 0.93 v4.0.0, 0.92 v3.7.0, 0.89 v3.4.0, 1.00 v3.3.0, 0.93 v3.1.0, 1.00 v2.2.1 -% Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 1 RR) -% Number of atoms : 3 ( 3 equality) -% Maximal clause size : 1 ( 1 average) -% Number of predicates : 1 ( 0 propositional; 2-2 arity) -% Number of functors : 3 ( 2 constant; 0-2 arity) -% Number of variables : 5 ( 0 singleton) -% Maximal term depth : 18 ( 8 average) -% SPC : CNF_UNS_RFO_PEQ_UEQ -% Comments : The problem was originally posed for cancellative semigroups, -% Otter does this with a nonstandard representation [MP96]. -cnf(assoc, axiom, '*'('*'(A,B),C)='*'(A,'*'(B,C))). -cnf(twiddle, axiom, '*'(A,'*'(B,'*'(B,B)))='*'(B,'*'(B,'*'(B,A)))). -cnf(conjecture, negated_conjecture, '*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,b))))))))))))))))) != '*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,b)))))))))))))))))). diff --git a/tests/vbool.p b/tests/vbool.p new file mode 100644 --- /dev/null +++ b/tests/vbool.p @@ -0,0 +1,18 @@ +fof(associativity, axiom, + ![X, Y, Z]: + X ⊕ (Y ⊕ Z) = (X ⊕ Y) ⊕ Z). + +fof(commutativity, axiom, + ![X, Y]: + X ⊕ Y = Y ⊕ X). + +fof(idempotence, axiom, + ![X]: + X ⊕ X = X). + +fof(non_injectivity, conjecture, + ![A, B]: ?[X]: A ⊕ X = B ⊕ X). + +% Examples: +% plus is commutative, associative, and injective, but not idempotent +% max is idempotent, commutative, and associativity, but not injective diff --git a/tests/veroff.p b/tests/veroff.p --- a/tests/veroff.p +++ b/tests/veroff.p @@ -7,10 +7,5 @@ cnf(associativity, axiom, f(f(X,W,Y),W,Z) = f(X,W,f(Y,W,Z))). -cnf(a123, axiom, f(a1,a2,a3) = f123). -cnf(a145, axiom, f(a1,a4,a5) = f145). -cnf(a245, axiom, f(a2,a4,a5) = f245). -cnf(a345, axiom, f(a3,a4,a5) = f345). -cnf(lhs, axiom, f(f123,a4,a5) = c1). -cnf(rhs, axiom, f(f145,f245,f345) = c2). -cnf(goal, axiom, c1 != c2). +cnf(dist_long, conjecture, + f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w))). diff --git a/tests/winker-easy.p b/tests/winker-easy.p new file mode 100644 --- /dev/null +++ b/tests/winker-easy.p @@ -0,0 +1,6 @@ +% Needs case split on X < c. +cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(idem, axiom, '+'(X, X) = X). +cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/winker.p b/tests/winker.p new file mode 100644 --- /dev/null +++ b/tests/winker.p @@ -0,0 +1,6 @@ +% Needs case split on X < c. +cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(idem_c, axiom, '+'(c, c) = c). +cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/winker2.p b/tests/winker2.p new file mode 100644 --- /dev/null +++ b/tests/winker2.p @@ -0,0 +1,6 @@ +% Needs case split on X < c. +cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(plus_c_d, axiom, '+'(c, d) = c). +cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/winkler-easy.p b/tests/winkler-easy.p deleted file mode 100644 --- a/tests/winkler-easy.p +++ /dev/null @@ -1,6 +0,0 @@ -% Needs case split on X < c. -cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)). -cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). -cnf(idem, axiom, '+'(X, X) = X). -cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). -cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/winkler.p b/tests/winkler.p deleted file mode 100644 --- a/tests/winkler.p +++ /dev/null @@ -1,6 +0,0 @@ -% Needs case split on X < c. -cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)). -cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). -cnf(idem_c, axiom, '+'(c, c) = c). -cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). -cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/winkler2.p b/tests/winkler2.p deleted file mode 100644 --- a/tests/winkler2.p +++ /dev/null @@ -1,6 +0,0 @@ -% Needs case split on X < c. -cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)). -cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). -cnf(plus_c_d, axiom, '+'(c, d) = c). -cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). -cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/y-easy.p b/tests/y-easy.p new file mode 100644 --- /dev/null +++ b/tests/y-easy.p @@ -0,0 +1,3 @@ +fof(k_def, axiom, ![X, Y]: (k @ X) @ Y = X). +fof(s_def, axiom, ![X, Y, Z]: ((s @ X) @ Y) @ Z = (X @ Z) @ (Y @ Z)). +fof(conjecture, conjecture, ![F]: ?[X]: F @ X = X). diff --git a/tests/y.p b/tests/y.p --- a/tests/y.p +++ b/tests/y.p @@ -1,3 +1,3 @@ -fof(k_def, axiom, ![X, Y]: '@'('@'(k, X), Y) = X). -fof(s_def, axiom, ![X, Y, Z]: '@'('@'('@'(s, X), Y), Z) = '@'('@'(X, Z), '@'(Y, Z))). -fof(conjecture, conjecture, ?[Y]: ![F]: '@'(Y, F) = '@'(F, '@'(Y, F))). +fof(k_def, axiom, ![X, Y]: (k @ X) @ Y = X). +fof(s_def, axiom, ![X, Y, Z]: ((s @ X) @ Y) @ Z = (X @ Z) @ (Y @ Z)). +fof(conjecture, conjecture, ?[Y]: ![F]: Y @ F = F @ (Y @ F)). diff --git a/twee.cabal b/twee.cabal --- a/twee.cabal +++ b/twee.cabal @@ -1,5 +1,5 @@ name: twee -version: 2.2 +version: 2.3 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3 @@ -36,15 +36,29 @@ description: Build a binary which statically links against libstdc++. default: False +flag parallel + description: Build a special parallel version of Twee. + default: False + executable twee - main-is: executable/Main.hs +-- if flag(parallel) +-- main-is: ParallelMain.hs +-- build-depends: async, unix +-- c-sources: executable/link.c +-- else + main-is: Main.hs + + hs-source-dirs: executable + other-modules: SequentialMain default-language: Haskell2010 build-depends: base < 5, - twee-lib == 2.2, + twee-lib == 2.3, containers, pretty, split, - jukebox == 0.4.* + jukebox == 0.5.*, + ansi-terminal >= 0.9, + symbol ghc-options: -W -fno-warn-incomplete-patterns if flag(static)