twee 2.2 → 2.3
raw patch · 51 files changed
+1921/−1048 lines, 51 filesdep +ansi-terminaldep +symboldep ~jukeboxdep ~twee-lib
Dependencies added: ansi-terminal, symbol
Dependency ranges changed: jukebox, twee-lib
Files
- README.md +1/−4
- executable/Main.hs +1/−692
- executable/SequentialMain.hs +914/−0
- misc/BestTwee.hs +157/−0
- misc/Localise.hs +114/−0
- misc/MaxCover.hs +63/−0
- tests/GRP666-4.p +63/−0
- tests/LAT071-1.p +37/−0
- tests/LAT073-1.p +37/−0
- tests/REL038-1.p +14/−0
- tests/RNG035-7.p +12/−0
- tests/ROB027-1.p +1/−7
- tests/append-rev.p +3/−3
- tests/blah.p +5/−0
- tests/db-goal.p +0/−22
- tests/db.p +26/−15
- tests/db2.p +29/−0
- tests/deriv.p +17/−19
- tests/diff.p +8/−4
- tests/factor.p +50/−0
- tests/fol.p +0/−16
- tests/group.p +14/−16
- tests/haken.p +170/−0
- tests/lat.p +0/−16
- tests/lcl.p +0/−7
- tests/loop-ascii.p +6/−0
- tests/loop.p +6/−6
- tests/loop2.p +6/−6
- tests/minus.p +5/−7
- tests/nand-goal.p +0/−44
- tests/nand.p +0/−37
- tests/nicomachus.p +36/−18
- tests/rel.p +32/−0
- tests/rel2.p +32/−0
- tests/ring-goal.p +0/−11
- tests/ring2-goal.p +0/−12
- tests/ring3-goal.p +0/−11
- tests/ring4-goal.p +0/−11
- tests/robbins-goal.p +0/−6
- tests/semigroup2.p +0/−26
- tests/vbool.p +18/−0
- tests/veroff.p +2/−7
- tests/winker-easy.p +6/−0
- tests/winker.p +6/−0
- tests/winker2.p +6/−0
- tests/winkler-easy.p +0/−6
- tests/winkler.p +0/−6
- tests/winkler2.p +0/−6
- tests/y-easy.p +3/−0
- tests/y.p +3/−3
- twee.cabal +18/−4
README.md view
@@ -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
executable/Main.hs view
@@ -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 "<module>" "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 "<function>" "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
+ executable/SequentialMain.hs view
@@ -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 "<axioms>" "expected a list of axiom names" Just)++ argModule = arg "<module>" "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 "<axioms>" "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 "<function>" "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
+ misc/BestTwee.hs view
@@ -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"]
+ misc/Localise.hs view
@@ -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'
+ misc/MaxCover.hs view
@@ -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
+ tests/GRP666-4.p view
@@ -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) )).++%------------------------------------------------------------------------------
+ tests/LAT071-1.p view
@@ -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)).++%--------------------------------------------------------------------------
+ tests/LAT073-1.p view
@@ -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)).++%--------------------------------------------------------------------------
+ tests/REL038-1.p view
@@ -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)).
+ tests/RNG035-7.p view
@@ -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).
tests/ROB027-1.p view
@@ -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
tests/append-rev.p view
@@ -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))).
+ tests/blah.p view
@@ -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)).
− tests/db-goal.p
@@ -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))).
tests/db.p view
@@ -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)).
+ tests/db2.p view
@@ -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)).
tests/deriv.p view
@@ -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)).
tests/diff.p view
@@ -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).
+ tests/factor.p view
@@ -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))).
− tests/fol.p
@@ -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).
tests/group.p view
@@ -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').
+ tests/haken.p view
@@ -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)).
− tests/lat.p
@@ -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))))))).
− tests/lcl.p
@@ -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).
+ tests/loop-ascii.p view
@@ -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)).
tests/loop.p view
@@ -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).
tests/loop2.p view
@@ -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).
tests/minus.p view
@@ -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').
− tests/nand-goal.p
@@ -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).--%--------------------------------------------------------------------------
− tests/nand.p
@@ -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))) )).--%--------------------------------------------------------------------------
tests/nicomachus.p view
@@ -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))).
+ tests/rel.p view
@@ -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)).
+ tests/rel2.p view
@@ -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).
− tests/ring-goal.p
@@ -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)).
− tests/ring2-goal.p
@@ -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').
− tests/ring3-goal.p
@@ -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)).
− tests/ring4-goal.p
@@ -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)).
− tests/robbins-goal.p
@@ -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).
− tests/semigroup2.p
@@ -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)))))))))))))))))).
+ tests/vbool.p view
@@ -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
tests/veroff.p view
@@ -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))).
+ tests/winker-easy.p view
@@ -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).
+ tests/winker.p view
@@ -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).
+ tests/winker2.p view
@@ -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).
− tests/winkler-easy.p
@@ -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).
− tests/winkler.p
@@ -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).
− tests/winkler2.p
@@ -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).
+ tests/y-easy.p view
@@ -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).
tests/y.p view
@@ -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)).
twee.cabal view
@@ -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)