packages feed

twee 2.4.2 → 2.5

raw patch · 23 files changed

+961/−53 lines, 23 filesdep +QuickCheckdep ~twee-lib

Dependencies added: QuickCheck

Dependency ranges changed: twee-lib

Files

executable/SequentialMain.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass #-}+{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass, RankNTypes #-} {-# OPTIONS_GHC -flate-specialise #-} module SequentialMain(main) where @@ -49,16 +49,18 @@     flags_flatten_nonground :: Bool,     flags_flatten_goals_lightly :: Bool,     flags_flatten_all :: Bool,+    flags_flatten_regeneralise :: Bool,     flags_eliminate :: [String],     flags_backwards_goal :: Int,     flags_flatten_backwards_goal :: Int,     flags_equals_transformation :: Bool,     flags_distributivity_heuristic :: Bool,-    flags_kbo_weight0 :: Bool }+    flags_kbo_weight0 :: Bool,+    flags_goal_heuristic :: Bool }  parseMainFlags :: OptionParser MainFlags parseMainFlags =-  MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenNonGround <*> flattenLightly <*> flattenAll <*> eliminate <*> backwardsGoal <*> flattenBackwardsGoal <*> equalsTransformation <*> distributivityHeuristic <*> kboWeight0+  MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenNonGround <*> flattenLightly <*> flattenAll <*> flattenRegeneralise <*> eliminate <*> backwardsGoal <*> flattenBackwardsGoal <*> equalsTransformation <*> distributivityHeuristic <*> kboWeight0 <*> goalHeuristic   where     proof =       inGroup "Output options" $@@ -106,6 +108,10 @@       expert $       inGroup "Completion heuristics" $       bool "flatten" ["Flatten all clauses by adding new axioms (off by default)."] False+    flattenRegeneralise =+      expert $+      inGroup "Completion heuristics" $+      bool "flatten-regeneralise" ["Regeneralise rules involving flattened goal terms (off by default)."] False     backwardsGoal =       expert $       inGroup "Completion heuristics" $@@ -122,6 +128,10 @@       expert $       inGroup "Completion heuristics" $       bool "distributivity-heuristic" ["Treat distributive operators specially (off by default)."] False+    goalHeuristic =+      expert $+      inGroup "Completion heuristics" $+      bool "goal-heuristic" ["Use the CP weighting heuristic from Anantharaman and Andrianarievelo (off by default)."] False     eliminate =       inGroup "Proof presentation" $       concat <$>@@ -136,10 +146,10 @@  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) <*>+  Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> maxRules <*> simplify <*> normPercent <*> cpSampleSize <*> cpRenormaliseThreshold <*> set_join_goals <*> always_simplify <*> complete_subsets <*>+    pure undefined <*> -- scoring function - filled in later, in runTwee     (Join.Config <$> ground_join <*> connectedness <*> ground_connectedness <*> set_join) <*>-    (Proof.Config <$> all_lemmas <*> flat_proof <*> ground_proof <*> show_instances <*> colour <*> show_axiom_uses)+    (Proof.Config <$> all_lemmas <*> flat_proof <*> ground_proof <*> show_instances <*> colour <*> show_axiom_uses) <*> pure [] <*> randomMode <*> randomModeGoalDirected <*> randomModeSimple <*> randomModeBestOf <*> alwaysComplete   where     maxSize =       inGroup "Resource limits" $@@ -151,6 +161,9 @@     maxCPDepth =       inGroup "Resource limits" $       flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum+    maxRules =+      inGroup "Resource limits" $+      flag "max-rules" ["Give up after generating this many rules (unlimited by default)."] maxBound argNum     simplify =       expert $       inGroup "Completion heuristics" $@@ -169,34 +182,6 @@       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" $@@ -272,6 +257,32 @@         (splitOn "," <$> arg "<axioms>" "expected a list of axiom names" Just)       where         interpret xss ax = axiom_name ax `elem` xss || "all" `elem` xss+    randomMode =+      expert $+      inGroup "Completion heuristics" $+      bool "random-mode"+        ["Use random testing to find suitable CPs (doesn't work yet!) (off by default)."]+        False+    randomModeGoalDirected =+      expert $+      inGroup "Completion heuristics" $+      bool "random-mode-goal-directed"+        ["Use goal-direction in --random-mode (off by default)."]+        False+    randomModeSimple =+      expert $+      inGroup "Completion heuristics" $+      bool "random-mode-simple"+        ["Use simple version of --random-mode (off by default)."]+        False+    randomModeBestOf =+      inGroup "Completion heuristics" $+      defaultFlag "random-mode-best-of" "Generate this many critical pairs at a time and pick the best one" cfg_random_mode_best_of argNum+    alwaysComplete =+      inGroup "Input and clausifier options" $+      bool "complete"+        ["Don't stop until the rewrite system is confluent"]+        False     colour = fromMaybe <$> io colourSupported <*> colourFlag     colourFlag =       inGroup "Proof presentation" $@@ -287,11 +298,50 @@       liftM2 (&&) (hSupportsANSIColor stdout)         (return (setSGRCode [] /= "")) -- Check for Windows terminal not supporting ANSI +    defaultFlag :: Show a => String -> String -> (Config Constant -> a) -> ArgParser a -> OptionParser a     defaultFlag name desc field parser =       flag name [desc ++ " (" ++ show def ++ " by default)."] def parser       where         def = field defaultConfig +parseCPConfig :: OptionParser CP.Config+parseCPConfig =+  CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor+  where+    lweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "lhs-weight" "Weight given to LHS of critical pair" CP.cfg_lhsweight argNum+    rweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "rhs-weight" "Weight given to RHS of critical pair" CP.cfg_rhsweight argNum+    funweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "fun-weight" "Weight given to function symbols" CP.cfg_funweight argNum+    varweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "var-weight" "Weight given to variable symbols" CP.cfg_varweight argNum+    depthweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "depth-weight" "Weight given to critical pair depth" CP.cfg_depthweight argNum+    dupcost =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "dup-cost" "Cost of duplicate subterms" CP.cfg_dupcost argNum+    dupfactor =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "dup-factor" "Size factor of duplicate subterms" CP.cfg_dupfactor argNum++    defaultFlag name desc field parser =+      flag name [desc ++ " (" ++ show def ++ " by default)."] def parser+      where+        def = field CP.defaultConfig+ parsePrecedence :: OptionParser [String] parsePrecedence =   expert $@@ -612,8 +662,8 @@       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 flags@MainFlags{..} later obligs = {-# SCC runTwee #-} do+runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> CP.Config -> MainFlags -> (IO () -> IO ()) -> Problem Clause -> IO Answer+runTwee globals (TSTPFlags tstp) horn precedence config0 cpConfig flags@MainFlags{..} later obligs = {-# SCC runTwee #-} do   let     -- Encode whatever needs encoding in the problem     obligs1@@ -651,9 +701,9 @@         (isType c)         (isNothing (elemIndex (base c) precedence))         (fmap negate (elemIndex (base c) precedence))-        (maybeNegate (Map.findWithDefault 0 c occs))+        (maybeNegate (Map.findWithDefault 0 c funOccs))     maybeNegate = if flags_flip_ordering then negate else id-    occs = funsOcc prob+    funOccs = funsOcc prob      -- Translate everything to Twee.     toEquation (t, u) =@@ -681,6 +731,28 @@     isDefinition Input{source = Unknown} = True     isDefinition inp = tag inp `elem` flags_eliminate +  -- Compute CP scoring heuristic+  let+    goalNests = nests (map goal_eqn goals)+    goalOccs = occs (map goal_eqn goals)+    score depth eqn+      | flags_goal_heuristic =+        fromIntegral (CP.score cpConfig depth eqn) *+        product+          [ pos (IntMap.findWithDefault 0 f eqnNests - IntMap.findWithDefault 0 f goalNests) *+            pos (IntMap.findWithDefault 0 f eqnOccs - IntMap.findWithDefault 0 f goalOccs)+          | f <- IntMap.keys eqnNests ] -- skip constants+      | otherwise = +        fromIntegral (CP.score cpConfig depth eqn)+      where+        eqnNests = nests eqn+        eqnOccs = occs eqn++        pos :: Int -> Float+        pos n = if n <= 0 then 1 else fromIntegral n+1+    config = config0 { cfg_score_cp = score, cfg_eliminate_axioms = if flags_flatten_regeneralise then defs else [] }++  let     withGoals = foldl' (addGoal config) (initialState config) goals     withAxioms = foldl' (addAxiom config) withGoals axioms     withBackwardsGoal = foldn rewriteGoalsBackwards withAxioms flags_backwards_goal@@ -982,6 +1054,7 @@            (combine <$>              expert hornToUnitBox <*>              parseConfig <*>+             parseCPConfig <*>              parseMainFlags <*>              (toFormulasBox =>>=               expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=@@ -989,7 +1062,7 @@              (runTwee <$> globalFlags <*> tstpFlags <*> expert hornFlags <*> parsePrecedence)))   profile   where-    combine horn config main encode prove later prob0 = do+    combine horn config cpConfig main encode prove later prob0 = do       res <- horn prob0       case res of         Left ans -> return ans@@ -1000,4 +1073,4 @@             isUnitEquality _ = False             isUnit = all isUnitEquality (map (toLiterals . what) prob0)             main' = if isUnit then main{flags_explain_encoding = False} else main{flags_formal_proof = False}-          encode prob >>= prove config main' later+          encode prob >>= prove config cpConfig main' later
misc/Test.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE TemplateHaskell, FlexibleInstances, FlexibleContexts, UndecidableInstances, StandaloneDeriving, ScopedTypeVariables, TupleSections, DeriveGeneric, DerivingVia, DeriveAnyClass #-}-module Test where+module Main where  import Twee.Constraints import Twee.Term hiding (subst, canonicalise, F)@@ -18,33 +18,48 @@ import qualified Data.Map as Map import Data.Maybe import Data.Ord-import Data.List+import Data.List hiding (singleton) import Data.Typeable import qualified Twee.Index as Index import Data.Int import GHC.Generics import Twee.Utils+import qualified Data.IntMap as M+import qualified Twee.Index as Index -data Func = F Int Integer deriving (Eq, Ord, Show)-  deriving Labelled via (AutoLabel Func)+data Func = F Int Integer deriving (Eq, Ord, Show, Labelled) -instance Pretty Func where pPrint (F f _) = text "f" <#> int f+instance Pretty Func where+  pPrint (F 3 _) = text "a"+  pPrint (F 4 _) = text "b"+  pPrint (F 5 _) = text "zero"+  pPrint (F 6 _) = text "plus"+  pPrint (F 7 _) = text "times"+  pPrint (F f _) = text "f" <#> int f instance PrettyTerm Func instance Arbitrary (Subst Func) where   arbitrary = fmap fromJust (fmap listToSubst (liftM2 zip (fmap nub arbitrary) (infiniteListOf arbitrary))) instance Arbitrary Func where-  arbitrary = F <$> choose (1, 1) <*> choose (1, 3)+  arbitrary = F <$> choose (0, 2) <*> choose (1, 3) instance Minimal Func where   minimal = fun (F 0 1) instance Ord.Sized Func where size (F _ n) = n instance Ord.Weighted Func where argWeight _ = 1+class Arity f where+  arity :: f -> Int instance Arity Func where   arity (F 0 _) = 0-  arity (F 1 _) = 2+  arity (F 1 _) = 1+  arity (F 2 _) = 2+  arity (F 3 _) = 0 -- a+  arity (F 4 _) = 0 -- b+  arity (F 5 _) = 0 -- zero+  arity (F 6 _) = 2 -- plus+  arity (F 7 _) = 2 -- times instance EqualsBonus Func  instance Arbitrary Var where arbitrary = fmap V (choose (0, 3))-instance (Labelled f, Ord f, Typeable f, Arbitrary f) => Arbitrary (Fun f) where+instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Fun f) where   arbitrary = fmap fun arbitrary  instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Term f) where@@ -52,7 +67,7 @@     sized $ \n ->       oneof $         [ build <$> var <$> arbitrary ] ++-        [ do { f <- arbitrary; build <$> app f <$> vectorOf (arity f) (resize ((n-1) `div` arity f) arbitrary :: Gen (Term f)) } | n > 0 ]+        [ do { f <- arbitrary; build <$> app (fun f) <$> vectorOf (arity f) (resize ((n-1) `div` arity f) arbitrary :: Gen (Term f)) } | n > 0 ]   shrink (App f ts0) =     ts ++ (build <$> app f <$> shrinkOne ts)     where@@ -63,6 +78,10 @@         [ x:ys | ys <- shrinkOne xs ]   shrink _ = [] +instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (TermList f) where+  arbitrary = buildList <$> listOf (arbitrary :: Gen (Term f))+  shrink = map buildList . shrink . unpack+ data Pair f = Pair (Term f) (Term f) deriving Show  instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Pair f) where@@ -221,8 +240,95 @@   counterexample (show eq) $   Ord.size (eqn_lhs eq') >= Ord.size (eqn_rhs eq') +--t :: Term Func+--t = build (app (fun (F 0)) [app (fun (F 1)) [var (V 0), var (V 1)], var (V 2)])++-- Define 'nest' from Fuchs "The application of goal-oriented heuristics...",+-- then refine it to a more efficient version+nestf :: Func -> Term Func -> Int+nestf f _ | arity f == 0 = 0+nestf f t = hnest (fun f) t 0 0+  where+    hnest _ (Var _) c a = max c a+    hnest _ (App _ Empty) c a = max c a+    hnest f (App g ts) c a+      | f == g = maximum [hnest f t (c+1) a | t <- unpack ts]+      | otherwise = maximum [hnest f t 0 (max c a) | t <- unpack ts]++-- a simpler version, to illustrate the meaning+nestf1 :: Func -> Term Func -> Int+nestf1 f t = hnest (fun f) t 0+  where+    hnest _ (Var _) c = c+    hnest _ (App _ Empty) c = c+    hnest f (App g ts) c+      | f == g = maximum [hnest f t (c+1) | t <- unpack ts]+      | otherwise = max c (maximum [hnest f t 0 | t <- unpack ts])++-- a more efficient version+nestf2 :: Func -> Term Func -> Int+nestf2 f t = hnest (fun f) (singleton t) 0 0+  where+    hnest _ Empty c a = max c a+    hnest f (Cons (Var _) ts) c a = hnest f ts c a+    hnest f (Cons (App _ Empty) ts) c a = hnest f ts c a+    hnest f (Cons (App g ts) us) c a+      | f == g = +        let a' = hnest f ts (c+1) a+        in hnest f us c a'+      | otherwise =+        let a' = hnest f ts 0 a+        in hnest f us c a'++-- a version that does all function symbols at once+nestf3 :: Term Func -> M.IntMap Int+nestf3 t = hnest 0 0 M.empty (singleton t)+  where+    hnest f c as Empty = M.insertWith max f c as+    hnest f c as (Cons (Var _) ts) = hnest f c as ts+    hnest f c as (Cons (App _ Empty) ts) = hnest f c as ts+    hnest f c as (Cons (App g ts) us) =+      let as' = hnest (fun_id g) (if f == fun_id g then c+1 else 1) as ts+      in hnest f c as' us++prop_nest_1 :: Func -> Term Func -> Property+prop_nest_1 f t = withMaxSuccess 1000000 $ nestf f t === nestf1 f t++prop_nest_2 :: Func -> Term Func -> Property+prop_nest_2 f t = withMaxSuccess 1000000 $ nestf f t === nestf2 f t++prop_nest_3 :: Func -> Term Func -> Property+prop_nest_3 f t =+  withMaxSuccess 1000000 $+    nestf f t === M.findWithDefault 0 (fun_id (fun f)) (nestf3 t)++prop_nests :: Func -> TermList Func -> Property+prop_nests f ts =+  withMaxSuccess 1000000 $+    maximum (0:map (nestf f) (unpack ts)) ===+    M.findWithDefault 0 (fun_id (fun f)) (nests ts)+ return [] main = $forAllProperties (quickCheckWithResult stdArgs { maxSuccess = 1000000 }) ---t :: Term Func---t = build (app (fun (F 0)) [app (fun (F 1)) [var (V 0), var (V 1)], var (V 2)])+a = con (fun (F 3 1))+b = con (fun (F 4 2))+zero = con (fun (F 5 1))+plus t u = app (fun (F 6 1)) [t, u]+times t u = app (fun (F 7 1)) [t, u]+x = var (V 0)+y = var (V 1)++axioms = [+  build (plus x y) ==== plus y x,+  times zero x ==== zero,+  plus x zero ==== x ]+  where+    t ==== u = build t :=: build u++rules = [orient eq (certify (axiom (Axiom 0 "axiom" eq))) | eq <- axioms]++theIndex = Index.fromList [(lhs r, r) | r <- rules]++term = build (plus (times zero a) b)+strat = anywhere1 (basic (rewrite reduces theIndex))
+ tests/LAT078-1.p view
@@ -0,0 +1,38 @@+%--------------------------------------------------------------------------+% File     : LAT078-1 : TPTP v9.0.0. Released v2.6.0.+% Domain   : Lattice Theory (Ortholattices)+% Problem  : Given single axiom MOL-27B2, prove associativity+% Version  : [MRV03] (equality) axioms.+% English  : Given a single axiom candidate MOL-27B2 for modular ortholattices+%            (MOL) 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    : MOL-27B2-associativity [MRV03]++% Status   : Unsatisfiable+% Rating   : 0.91 v8.2.0, 0.96 v8.1.0, 0.95 v7.5.0, 0.96 v7.4.0, 1.00 v7.3.0, 0.95 v7.1.0, 0.94 v7.0.0, 0.95 v6.4.0, 1.00 v2.6.0+% Syntax   : Number of clauses     :    2 (   2 unt;   0 nHn;   1 RR)+%            Number of literals    :    2 (   2 equ;   1 neg)+%            Maximal clause size   :    1 (   1 avg)+%            Maximal term depth    :    9 (   2 avg)+%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)+%            Number of functors    :    4 (   4 usr;   3 con; 0-2 aty)+%            Number of variables   :    4 (   1 sgn)+% SPC      : CNF_UNS_RFO_PEQ_UEQ++% Comments :+%--------------------------------------------------------------------------+%----Single axiom MOL-27B2+cnf(mol_27B2,axiom,+    f(f(f(f(B,A),f(A,C)),D),f(A,f(f(f(B,f(B,f(f(C,C),A))),A),C))) = 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(not, axiom,+    not(X) = f(X,X)).
+ tests/ROB007-1-a.p view
@@ -0,0 +1,12 @@+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).+cnf(associativity_of_add, axiom, add(add(X, Y), Z)=add(X, add(Y, Z))).+cnf(robbins_axiom, axiom, inv(add(inv(add(X, Y)), inv(add(X, inv(Y)))))=X).+cnf(condition, hypothesis, inv(add(a, b))=inv(b)).+cnf(prove_huntingtons_axiom, negated_conjecture, add(inv(add(a, inv(b))), inv(add(inv(a), inv(b))))!=b).++cnf(sos04,axiom,(+    g(A) = inv(add(A,inv(A))) )).++%----Definition of h+cnf(sos05,axiom,(+    h(A) = add(A,add(A,add(A,inv(add(A,inv(A)))))))).
+ tests/ROB007-1.p view
@@ -0,0 +1,5 @@+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).+cnf(associativity_of_add, axiom, add(add(X, Y), Z)=add(X, add(Y, Z))).+cnf(robbins_axiom, axiom, negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).+cnf(condition, hypothesis, negate(add(a, b))=negate(b)).+cnf(prove_huntingtons_axiom, negated_conjecture, add(negate(add(a, negate(b))), negate(add(negate(a), negate(b))))!=b).
+ tests/ROB027-1-inv.p view
@@ -0,0 +1,58 @@+%--------------------------------------------------------------------------+% File     : ROB027-1 : TPTP v6.3.0. Released v1.2.0.+% Domain   : Robbins Algebra+% Problem  : -(-c) = c => Boolean+% Version  : [Win90] (equality) axioms.+%            Theorem formulation : Denies Huntington's axiom.+% English  : If there are elements c and d such that c+d=d, then the+%            algebra is Boolean.++% Refs     : [HMT71] Henkin et al. (1971), Cylindrical Algebras+%          : [Win90] Winker (1990), Robbins Algebra: Conditions that make a+%          : [Wos94] Wos (1994), Two Challenge Problems+% Source   : [Wos94]+% Names    : - [Wos94]++% Status   : Open+% Rating   : 1.00 v2.0.0+% Syntax   : Number of clauses     :    5 (   0 non-Horn;   5 unit;   2 RR)+%            Number of atoms       :    5 (   5 equality)+%            Maximal clause size   :    1 (   1 average)+%            Number of predicates  :    1 (   0 propositional; 2-2 arity)+%            Number of functors    :    5 (   3 constant; 0-2 arity)+%            Number of variables   :    7 (   0 singleton)+%            Maximal term depth    :    6 (   3 average)+% SPC      : CNF_UNK_UEQ++% Comments : Commutativity, associativity, and Huntington's axiom+%            axiomatize Boolean algebra.+%--------------------------------------------------------------------------+%----Include axioms for Robbins algebra+%--------------------------------------------------------------------------+cnf(commutativity_of_add,axiom,+    ( add(X,Y) = add(Y,X) )).++cnf(associativity_of_add,axiom,+    ( add(add(X,Y),Z) = add(X,add(Y,Z)) )).++cnf(robbins_axiom,axiom,+    ( inv(add(inv(add(X,Y)),inv(add(X,inv(Y))))) = X )).++%--------------------------------------------------------------------------+%--------------------------------------------------------------------------+cnf(double_negation,hypothesis,+    ( inv(inv(c)) = c )).++cnf(prove_huntingtons_axiom,negated_conjecture,+    add(inv(add(a,inv(b))),inv(add(inv(a),inv(b)))) != b).++%--------------------------------------------------------------------------+%----Definition of g+cnf(sos04,axiom,(+    g(A) = inv(add(A,inv(A))) )).++%----Definition of h+cnf(sos05,axiom,(+    h(A) = add(A,add(A,add(A,inv(add(A,inv(A)))))))).++cnf(sos06, axiom, i(X,Y) = inv(add(X, inv(add(X, Y))))).
+ tests/aim.p view
@@ -0,0 +1,62 @@+cnf(left_ident, axiom,+  '1' * X = X).+cnf(right_ident, axiom,+  X * '1' = X).+cnf(left_division_1, axiom,+  X \ (X * Y) = Y).+cnf(left_division_2, axiom,+  X * (X \ Y) = Y).+cnf(right_division_1, axiom,+  (X * Y) / Y = X).+cnf(right_division_2, axiom,+  (X / Y) * Y = X).+cnf(associator, axiom,+  (X * (Y * Z)) \ ((X * Y) * Z) = a(X,Y,Z)).+cnf(commutator, axiom,+  (X * Y) \ (Y * X) = k(Y,X)).+cnf(l, axiom,+  (Y * X) \ (Y * (X * U)) = l(U,X,Y)).+cnf(r, axiom,+  ((U * X) * Y) / (X * Y) = r(U,X,Y)).+cnf(t, axiom,+  X \ (U * X) = t(U,X)).+cnf(abelian_inner_mapping_1, axiom,+  t(t(U,X),Y) = t(t(U,Y),X)).+cnf(abelian_inner_mapping_2, axiom,+  t(l(U,X,Y),Z) = l(t(U,Z),X,Y)).+cnf(abelian_inner_mapping_3, axiom,+  t(r(U,X,Y),Z) = r(t(U,Z),X,Y)).+cnf(abelian_inner_mapping_4, axiom,+  l(r(U,X,Y),Z,W) = r(l(U,Z,W),X,Y)).+cnf(abelian_inner_mapping_5, axiom,+  l(l(U,X,Y),Z,W) = l(l(U,Z,W),X,Y)).+cnf(abelian_inner_mapping_6, axiom,+  r(r(U,X,Y),Z,W) = r(r(U,Z,W),X,Y)).++% aK (or "single-a") goals+cnf(ka, conjecture,+  k(a(X,Y,Z),U) = '1').+cnf(aK1, conjecture,+  a(k(X,Y),Z,U) = '1').+cnf(aK2, conjecture,+  a(X,k(Y,Z),U) = '1').+cnf(aK3, conjecture,+  a(X,Y,k(Z,U)) = '1').++% aa (or "double-a") goals+cnf(aa1, conjecture,+  a(a(X,Y,Z),U,W) = '1').+cnf(aa2, conjecture,+  a(X,a(Y,Z,U),W) = '1').+cnf(aa3, conjecture,+  a(X,Y,a(Z,U,W)) = '1').++%cnf(everything, conjecture,+%  k(a(X,Y,Z),U) = '1' |+%  a(k(X,Y),Z,U) = '1' |+%  a(X,k(Y,Z),U) = '1' |+%  a(X,Y,k(Z,U)) = '1' |+%  a(a(X,Y,Z),U,W) = '1' |+%  a(X,a(Y,Z,U),W) = '1' |+%  a(X,Y,a(Z,U,W)) = '1').+
+ tests/aim2.p view
@@ -0,0 +1,64 @@+cnf(left_ident, axiom,+  '1' * X = X).+cnf(right_ident, axiom,+  X * '1' = X).+cnf(left_division_1, axiom,+  X \ (X * Y) = Y).+cnf(left_division_2, axiom,+  X * (X \ Y) = Y).+cnf(right_division_1, axiom,+  (X * Y) / Y = X).+cnf(right_division_2, axiom,+  (X / Y) * Y = X).+cnf(associator, axiom,+  (X * (Y * Z)) \ ((X * Y) * Z) = a(X,Y,Z)).+cnf(commutator, axiom,+  (X * Y) \ (Y * X) = k(Y,X)).+cnf(l, axiom,+  (Y * X) \ (Y * (X * U)) = l(U,X,Y)).+cnf(r, axiom,+  ((U * X) * Y) / (X * Y) = r(U,X,Y)).+cnf(t, axiom,+  X \ (U * X) = t(U,X)).+cnf(abelian_inner_mapping_1, axiom,+  t(t(U,X),Y) = t(t(U,Y),X)).+cnf(abelian_inner_mapping_2, axiom,+  t(l(U,X,Y),Z) = l(t(U,Z),X,Y)).+cnf(abelian_inner_mapping_3, axiom,+  t(r(U,X,Y),Z) = r(t(U,Z),X,Y)).+cnf(abelian_inner_mapping_4, axiom,+  l(r(U,X,Y),Z,W) = r(l(U,Z,W),X,Y)).+cnf(abelian_inner_mapping_5, axiom,+  l(l(U,X,Y),Z,W) = l(l(U,Z,W),X,Y)).+cnf(abelian_inner_mapping_6, axiom,+  r(r(U,X,Y),Z,W) = r(r(U,Z,W),X,Y)).++% aK (or "single-a") goals+cnf(ka, conjecture,+  k(a(X,Y,Z),U) = '1').+cnf(aK1, conjecture,+  a(k(X,Y),Z,U) = '1').+cnf(aK2, conjecture,+  a(X,k(Y,Z),U) = '1').+cnf(aK3, conjecture,+  a(X,Y,k(Z,U)) = '1').++% aa (or "double-a") goals+cnf(aa1, conjecture,+  a(a(X,Y,Z),U,W) = '1').+cnf(aa2, conjecture,+  a(X,a(Y,Z,U),W) = '1').+cnf(aa3, conjecture,+  a(X,Y,a(Z,U,W)) = '1').++%cnf(everything, conjecture,+%  k(a(X,Y,Z),U) = '1' |+%  a(k(X,Y),Z,U) = '1' |+%  a(X,k(Y,Z),U) = '1' |+%  a(X,Y,k(Z,U)) = '1' |+%  a(a(X,Y,Z),U,W) = '1' |+%  a(X,a(Y,Z,U),W) = '1' |+%  a(X,Y,a(Z,U,W)) = '1').+++cnf(bonus, axiom, (X * (Y / X)) \ X = Y \ (Y / (Y / X))).
+ tests/diff2.p view
@@ -0,0 +1,34 @@+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(empty, axiom,+    X \ empty = X).++cnf(equals, conjecture,+    (X \ Y = empty & Y \ X = empty) => X = Y).++cnf(union, axiom,+    X \ union(Y, Z) = (X \ Y) \ Z).++cnf(union, conjecture,+    union(a,b) = union(b,a)).+cnf(union, conjecture,+    union(a,a) = a).+cnf(union, conjecture,+    union(a,union(b,c)) = union(union(a,b),c)).++cnf(intersection, axiom,+    intersection(X, Y) = X \ (X \ Y)).++cnf(intersection, conjecture,+    intersection(a,b) = intersection(b,a)).+cnf(intersection, conjecture,+    intersection(a,a) = a).+cnf(intersection, conjecture,+    intersection(a,intersection(b,c)) = intersection(intersection(a,b),c)).+cnf(intersection, conjecture,+    intersection(X, Y) = union(X,Y) \ union(X \ Y, Y \ X)).
+ tests/filter.p view
@@ -0,0 +1,59 @@+fof('associativity of ∘', axiom,+    ![F, G, H]:+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).++fof('∘ identity', axiom,+    ![F]:+    id ∘ F = F).++fof('∘ identity', axiom,+    ![F]:+    F ∘ id = F).++fof('map functor', axiom,+    ![F, G]:+    map(F) ∘ map(G) = map(F ∘ G)).++fof('map functor', axiom,+    map(id) = id).++fof('naturality of concat', axiom,+    ![F]:+    map(F) ∘ concat = concat ∘ map(map(F))).++fof('defn filter', axiom,+    ![P]:+    filter(P) = concat ∘ map(test(P))).++% test(P) = \x -> if P(x) then [x] else []++fof('test property', axiom,+    ![P, F]:+    test(P) ∘ F =+    map(F) ∘ test(P ∘ F)).++fof('map/filter', conjecture,+    ![P, F]:+    filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).+++% cond(P, F, G) = \x -> if P(x) then F(x) else G(x)++%fof('test defn', axiom,+%    ![P]:+%    test(P) = cond(P, unit, nil)).+%fof('cond ∘', axiom,+%    ![F, P, G, H]:+%    F ∘ cond(P, G, H) = cond(P, F ∘ G, F ∘ H)).+%fof('cond ∘', axiom,+%    ![F, P, G, H]:+%    cond(P, G, H) ∘ F = cond(P ∘ F, G ∘ F, H ∘ F)).+%fof('nil', axiom,+%    ![F]:+%    nil ∘ F = nil).+%fof('nil', axiom,+%    ![F]:+%    map(F) ∘ nil = nil).+%fof('unit', axiom,+%    ![F]:+%    map(F) ∘ unit = unit ∘ F).
+ tests/filter2.p view
@@ -0,0 +1,59 @@+fof('associativity of ∘', axiom,+    ![F, G, H]:+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).++fof('∘ identity', axiom,+    ![F]:+    id ∘ F = F).++fof('∘ identity', axiom,+    ![F]:+    F ∘ id = F).++fof('map functor', axiom,+    ![F, G]:+    map(F) ∘ map(G) = map(F ∘ G)).++fof('map functor', axiom,+    map(id) = id).++fof('naturality of concat', axiom,+    ![F]:+    map(F) ∘ concat = concat ∘ map(map(F))).++fof('defn filter', axiom,+    ![P]:+    filter(P) = concat ∘ map(test(P))).++% test(P) = \x -> if P(x) then [x] else []++%fof('test property', axiom,+%    ![P, F]:+%    test(P) ∘ F =+%    map(F) ∘ test(P ∘ F)).++fof('map/filter', conjecture,+    ![P, F]:+    filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).+++% cond(P, F, G) = \x -> if P(x) then F(x) else G(x)++fof('test defn', axiom,+    ![P]:+    test(P) = cond(P, unit, nil)).+fof('cond ∘', axiom,+    ![F, P, G, H]:+    F ∘ cond(P, G, H) = cond(P, F ∘ G, F ∘ H)).+fof('cond ∘', axiom,+    ![F, P, G, H]:+    cond(P, G, H) ∘ F = cond(P ∘ F, G ∘ F, H ∘ F)).+fof('nil', axiom,+    ![F]:+    nil ∘ F = nil).+fof('nil', axiom,+    ![F]:+    map(F) ∘ nil = nil).+fof('unit', axiom,+    ![F]:+    map(F) ∘ unit = unit ∘ F).
+ tests/lukasiewicz2.p view
@@ -0,0 +1,5 @@+cnf(detachment, axiom, (p(X) & p(i(X,Y))) => p(Y)).+cnf(lukasiewicz, axiom, p(i(i(i(P,Q),R),i(i(R,P),i(S,P))))).+cnf(simp, axiom, p(i(P, i(Q, Q)))).+cnf(peirce, axiom, p(i(i(i(P,Q),P),P))).+cnf(syll, conjecture, p(i(i(a,b),i(i(b,c),i(a,c))))).
+ tests/p.p view
@@ -0,0 +1,11 @@+cnf(a, axiom, p(X)!=true | p(s(X))!=true).+cnf(a, axiom, p(X)!=false | p(s(X))!=false).+cnf(a, axiom, p(a)=true).+cnf(a, axiom, p(s(s(a)))!=true).+cnf(a, axiom, true!=false).++cnf(p, axiom, p(a)=true).+cnf(p, axiom, p(s(a))=true).+cnf(p, axiom, p(s(s(a)))=false).+cnf(p, axiom, p(s(s(s(a))))=true).+cnf(p, axiom, p(s(s(s(X))))=false => p(s(s(s(s(X)))))=true).
+ tests/regexp.p view
@@ -0,0 +1,54 @@+%% and, or+cnf(def, axiom, and(true,B) = B).+cnf(def, axiom, and(false,B) = false).+cnf(def, axiom, and(X,Y) = and(Y,X)).++cnf(def, axiom, or(true,B) = true).+cnf(def, axiom, or(false,B) = B).+cnf(def, axiom, or(X,Y) = or(Y,X)).++%% eq+cnf(def, axiom, eq(X,X) = true).+cnf(def, axiom, eq(X,Y) = eq(Y,X)).+cnf(def, axiom, eq(a,b) = false).+cnf(def, axiom, eq(a,c) = false).+cnf(def, axiom, eq(b,c) = false).++%% haseps+cnf(def, axiom, haseps(atom(A)) = false).+cnf(def, axiom, haseps(zero) = false).+cnf(def, axiom, haseps(eps) = true).+cnf(def, axiom, haseps(plus(P,Q)) = or(haseps(P),haseps(Q))).+cnf(def, axiom, haseps(seq(P,Q)) = and(haseps(P),haseps(Q))).+cnf(def, axiom, haseps(star(P)) = true).++%% step+cnf(def, axiom, step(atom(A),A) = eps).+cnf(def, axiom, eq(A,B) = false => step(atom(A),B) = zero).+cnf(def, axiom, step(zero,B) = zero).+cnf(def, axiom, step(eps,B) = zero).+cnf(def, axiom, step(plus(P,Q),B) = plus(step(P,B),step(Q,B))).+cnf(def, axiom, haseps(P) = true => step(seq(P,Q),B) = plus(seq(step(P,B),Q),step(Q,B))).+cnf(def, axiom, haseps(P) = false => step(seq(P,Q),B) = plus(seq(step(P,B),Q),zero)).+cnf(def, axiom, step(star(P),B) = seq(step(P,B),star(P))).++%% rec+cnf(def, axiom, rec(P,nil) = haseps(P)).+cnf(def, axiom, rec(P,cons(A,As)) = rec(step(P,A),As)).++%% question+cnf(hypothesis, axiom, rec(seq(P,Q), As) = rec(seq(Q,P), As)).+cnf(goal, axiom, true != false).++%cnf(a, axiom, atom(A) != zero & atom(A) != eps & atom(A) != plus(P, Q) & atom(A) != seq(P, Q) & atom(A) != star(P)).+%cnf(a, axiom, zero != eps & zero != plus(P, Q) & zero != seq(P, Q) & zero != star(P)).+%cnf(a, axiom, eps != plus(P, Q) & eps != seq(P, Q) & eps != star(P)).+%cnf(a, axiom, plus(P, Q) != seq(P, Q) & plus(P, Q) != star(P)).+%cnf(a, axiom, seq(P, Q) != star(P)).+%cnf(a, axiom, un_atom(atom(A)) = A).+%cnf(a, axiom, un_plus_1(plus(P, Q)) = P).+%cnf(a, axiom, un_plus_2(plus(P, Q)) = Q).+%cnf(a, axiom, un_seq_1(seq(P, Q)) = P).+%cnf(a, axiom, un_seq_2(seq(P, Q)) = Q).+%cnf(a, axiom, un_star(star(P)) = P).+%cnf(a, axiom, a != b & b != c & a != c).
+ tests/sudoku.p view
@@ -0,0 +1,39 @@+cnf('associativity of ∘', axiom,+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).++cnf('∘ identity', axiom,+    id ∘ F = F).++cnf('∘ identity', axiom,+    F ∘ id = F).++cnf('map functor', axiom,+    map(F) ∘ map(G) = map(F ∘ G)).++cnf('map functor', axiom,+    map(id) = id).++cnf('defn pruneBy', axiom,+    pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).++cnf('defn expand', axiom,+    expand = product ∘ map(product)).++cnf('expand after boxs', axiom,+    expand ∘ boxs = map(boxs) ∘ expand).++cnf('filter with boxs', axiom,+    filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).++cnf('boxs involution', axiom,+    boxs ∘ boxs = id).++cnf('filter after product', axiom,+    filter(all(P)) ∘ product = product ∘ map(filter(P))).++cnf('law of pruneRow', axiom,+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).++cnf('conjecture', conjecture,+    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =+    filter(all(nodups) ∘ boxs) ∘ expand).
+ tests/sudoku2.p view
@@ -0,0 +1,44 @@+cnf('associativity of ∘', axiom,+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).++cnf('∘ identity', axiom,+    id ∘ F = F).++cnf('∘ identity', axiom,+    F ∘ id = F).++cnf('map functor', axiom,+    map(F) ∘ map(G) = map(F ∘ G)).++cnf('map functor', axiom,+    map(id) = id).++cnf('defn pruneBy', axiom,+    pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).++cnf('defn expand', axiom,+    expand = product ∘ map(product)).++cnf('expand after boxs', axiom,+    expand ∘ boxs = map(boxs) ∘ expand).++cnf('filter with boxs', axiom,+    filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).++cnf('boxs involution', axiom,+    boxs ∘ boxs = id).++cnf('filter after product', axiom,+    filter(all(P)) ∘ product = product ∘ map(filter(P))).++cnf('law of pruneRow', axiom,+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).++cnf('lhs', axiom,+    lhs = filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs))).++cnf('rhs', axiom,+    rhs = filter(all(nodups) ∘ boxs) ∘ expand).++cnf('conjecture', conjecture,+    lhs = rhs).
+ tests/sudoku3.p view
@@ -0,0 +1,42 @@+cnf('associativity of ∘', axiom,+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).++cnf('∘ identity', axiom,+    id ∘ F = F).++cnf('∘ identity', axiom,+    F ∘ id = F).++cnf('map functor', axiom,+    map(F) ∘ map(G) = map(F ∘ G)).++cnf('map functor', axiom,+    map(id) = id).++cnf('defn pruneBy', axiom,+    pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).++cnf('defn expand', axiom,+    expand = product ∘ map(product)).++cnf('expand after boxs', axiom,+    expand ∘ boxs = map(boxs) ∘ expand).++cnf('filter with boxs', axiom,+    filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).++cnf('boxs involution', axiom,+    boxs ∘ boxs = id).++cnf('filter after product', axiom,+    filter(all(P)) ∘ product = product ∘ map(filter(P))).++cnf('law of pruneRow', axiom,+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).++cnf('map/filter', axiom,+    filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).++cnf('conjecture', conjecture,+    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =+    filter(all(nodups) ∘ boxs) ∘ expand).
+ tests/sudoku4.p view
@@ -0,0 +1,45 @@+fof('associativity of ∘', axiom,+    ![F,G,H]: F ∘ (G ∘ H) = (F ∘ G) ∘ H).++fof('∘ identity', axiom,+    ![F]: id ∘ F = F).++fof('∘ identity', axiom,+    ![F]: F ∘ id = F).++fof('map functor', axiom,+    ![F, G]: map(F) ∘ map(G) = map(F ∘ G)).++fof('map functor', axiom,+    map(id) = id).++fof('defn pruneBy', axiom,+    ![F]: pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).++fof('defn expand', axiom,+    expand = product ∘ map(product)).++fof('expand after boxs', axiom,+    expand ∘ boxs = map(boxs) ∘ expand).++fof('filter with boxs', axiom,+    ![P, F]: filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).++fof('boxs involution', axiom,+    boxs ∘ boxs = id).++fof('filter after product', axiom,+    ![P]: filter(all(P)) ∘ product = product ∘ map(filter(P))).++fof('law of pruneRow', axiom,+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).++fof('map/filter', axiom,+    ![P, F]: filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).++fof('product/map', axiom,+    ![F]: product ∘ map(F) = map(map(F)) ∘ product).++fof('conjecture', conjecture,+    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =+    filter(all(nodups) ∘ boxs) ∘ expand).
+ tests/sudoku5.p view
@@ -0,0 +1,42 @@+cnf('associativity of ∘', axiom,+    F ∘ (G ∘ H) = (F ∘ G) ∘ H).++cnf('∘ identity', axiom,+    id ∘ F = F).++cnf('∘ identity', axiom,+    F ∘ id = F).++cnf('map functor', axiom,+    map(F) ∘ map(G) = map(F ∘ G)).++cnf('map functor', axiom,+    map(id) = id).++cnf('defn pruneBy', axiom,+    pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).++cnf('defn expand', axiom,+    expand = product ∘ map(product)).++cnf('expand after boxs', axiom,+    expand ∘ boxs = map(boxs) ∘ expand).++cnf('filter with boxs', axiom,+    filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).++cnf('boxs involution', axiom,+    boxs ∘ boxs = id).++cnf('filter after product', axiom,+    filter(all(P)) ∘ product = product ∘ map(filter(P))).++cnf('law of pruneRow', axiom,+    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).++cnf('product/map', axiom,+    product ∘ map(F) = map(map(F)) ∘ product).++cnf('conjecture', conjecture,+    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =+    filter(all(nodups) ∘ boxs) ∘ expand).
+ tests/union.p view
@@ -0,0 +1,9 @@+cnf(elem_union_1, axiom, notelem(X, A) | ~notelem(X, union(A, B))).+cnf(elem_union_2, axiom, notelem(X, B) | ~notelem(X, union(A, B))).+cnf(elem_union_3, axiom, notelem(X, union(A, B)) | ~notelem(X, A) | ~notelem(X, B)).+cnf(elem_equals, axiom, A=B | ~notelem(sK1_elem_equals_X(A, B), A) | ~notelem(sK1_elem_equals_X(A, B), B)).+cnf(union_commutative, negated_conjecture, union(a, b)!=union(b, a)).++cnf(elem_equals_1, axiom, choice(A,B) = c1 => notelem(sK1_elem_equals_X(A, B), A)).+cnf(elem_equals_2, axiom, choice(A,B) = c2 => notelem(sK1_elem_equals_X(A, B), B)).+cnf(elem_equals_3, axiom, choice(A,B) = c3 => A=B).
+ tests/union2.p view
@@ -0,0 +1,25 @@+cnf(ifeq_axiom, axiom, ifeq4(A, A, B, C)=B).+cnf(ifeq_axiom, axiom, ifeq3(A, A, B, C)=B).+cnf(ifeq_axiom, axiom, ifeq2(A, A, B, C)=B).+cnf(ifeq_axiom, axiom, ifeq(A, A, B, C)=B).+cnf(elem_union_1, axiom, ifeq(notelem(X, union(A, B)), true, notelem(X, A), true)=true).+cnf(elem_union_2, axiom, ifeq(notelem(X, union(A, B)), true, notelem(X, B), true)=true).+cnf(elem_union_3, axiom, ifeq(notelem(X, B), true, ifeq(notelem(X, A), true, notelem(X, union(A, B)), true), true)=true).+cnf(elem_equals, axiom, ifeq2(notelem(sK1_elem_equals_X(A, B), B), true, ifeq2(notelem(sK1_elem_equals_X(A, B), A), true, A, B), B)=B).+%cnf(union_commutative, negated_conjecture, union(a, b)!=union(b, a)).+%cnf(elem_equals_1, axiom, ifeq3(choice(A, B), c1, notelem(sK1_elem_equals_X(A, B), A), true)=true).+%cnf(elem_equals_2, axiom, ifeq3(choice(A, B), c2, notelem(sK1_elem_equals_X(A, B), B), true)=true).+%cnf(elem_equals_3, axiom, ifeq4(choice(A, B), c3, A, B)=B).+cnf(elem_equals_1, axiom, select(c1, a, d, d) = d).+cnf(elem_equals_1, axiom, select(c2, d, b, d) = d).+cnf(elem_equals_1, axiom, select(c3, d, d, c) = d).+cnf(blah, conjecture, a=d | b=d | c=d).+cnf(select, axiom, select(C, X, X, X)=X).+cnf(select, axiom, select(c1, X, Y, Z)=X).+cnf(select, axiom, select(c2, X, Y, Z)=Y).+cnf(select, axiom, select(c3, X, Y, Z)=Z).++%select(C, X, Y, Z) = select(C, select(c1, X, Y, Z), select(c2, X, Y, Z), select(c3, X, Y, Z)).++%  d+%= select(
+ tests/y-i.p view
@@ -0,0 +1,4 @@+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(i_def, axiom, ![X]: i @ X = X).+fof(conjecture, conjecture, ?[Y]: ![F]: Y @ F = F @ (Y @ F)).
twee.cabal view
@@ -1,5 +1,5 @@ name:                twee-version:             2.4.2+version:             2.5 synopsis:            An equational theorem prover homepage:            http://github.com/nick8325/twee license:             BSD3@@ -38,6 +38,11 @@   default: False   manual: True +flag parallel+  description: Build a special parallel version of Twee.+  default: False+  manual: True+ executable twee   main-is: Main.hs @@ -45,7 +50,7 @@   other-modules:       SequentialMain   default-language:    Haskell2010   build-depends:       base < 5,-                       twee-lib == 2.4.2,+                       twee-lib == 2.5,                        containers,                        pretty,                        split,@@ -59,3 +64,16 @@    if flag(static-cxx)     ghc-options: -pgml misc/static-libstdc++++Test-Suite twee-test+    type: exitcode-stdio-1.0+    Default-language: Haskell2010+    hs-source-dirs:+        misc+    main-is: Test.hs+    build-depends: base < 5, QuickCheck, twee-lib == 2.5, containers, pretty+    ghc-options:+      -threaded+      -rtsopts+      -feager-blackholing+      -with-rtsopts=-N4