diff options
| author | NickSmallbone <> | 2021-04-07 14:51:00 (GMT) |
|---|---|---|
| committer | hdiff <hdiff@hdiff.luite.com> | 2021-04-07 14:51:00 (GMT) |
| commit | 645622117e2ffbe4ac7649efb84fa1d5bef68d99 (patch) | |
| tree | a7b28a9409dfb4c36178be1cf3d4cc32831af2f1 | |
| parent | c42f93101a73db02cc601001eb82ad795d268bfb (diff) | |
40 files changed, 1191 insertions, 64 deletions
diff --git a/executable/SequentialMain.hs b/executable/SequentialMain.hs index dae2da5..8128825 100644 --- a/executable/SequentialMain.hs +++ b/executable/SequentialMain.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards #-} +{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DerivingVia #-} {-# OPTIONS_GHC -flate-specialise #-} module SequentialMain(main) where @@ -24,7 +24,7 @@ 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.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size, Subst, subst) import Jukebox.Tools.EncodeTypes import Jukebox.TPTP.Print import Jukebox.Tools.HornToUnit @@ -283,14 +283,11 @@ data Constant = con_weight :: !Integer, con_bonus :: !Bool } deriving (Eq, Ord) + deriving Labelled via AutoLabel Constant 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 @@ -351,9 +348,8 @@ data TweeContext = 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) + | otherwise = Constant prec fun (Jukebox.arity fun) 1 1 (bonus fun) where - sz fun = {-if isType fun then 0 else-} 1 bonus fun = (isIfeq fun && encoding flags /= Asymmetric2) || SequentialMain.isEquals fun @@ -549,7 +545,7 @@ runTwee globals (TSTPFlags tstp) horn precedence config MainFlags{..} later obli | otherwise = x prob = prettyNames (mapName lowercaseSkolem (addNarrowing ctx obligs')) - (axioms0, goals0) <- + (unsortedAxioms0, goals0) <- case identifyProblem ctx prob of Left inp -> do mapM_ (hPutStrLn stderr) [ @@ -574,25 +570,27 @@ runTwee globals (TSTPFlags tstp) horn precedence config MainFlags{..} later obli toEquation (t, u) = canonicalise (tweeTerm horn ctx prec t :=: tweeTerm horn ctx prec u) + axiomCompare ax1 ax2 + | ax1' `simplerThan` ax2' = LT + | ax2' `simplerThan` ax1' = GT + | otherwise = EQ + where + ax1' = toEquation (pre_eqn ax1) + ax2' = toEquation (pre_eqn ax2) + axioms0 = sortBy axiomCompare unsortedAxioms0 + 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) ] + | (n, PreEquation{..}) <- zip [1..] axioms0 ] defs = [ axiom - | (axiom, PreEquation{..}) <- zip axioms (sortBy axiomCompare axioms0), + | (axiom, PreEquation{..}) <- zip axioms 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 @@ -827,29 +825,30 @@ presentToJukebox ctx toEquation axioms goals Presentation{..} = 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 = + deriv p = Input { tag = "step", kind = Jukebox.Ax Jukebox.Axiom, what = jukeboxEquation (equation (certify p)), source = - Inference "rw" "thm" sources } + Inference name "thm" sources } + where + (name, sources) = unpack p + + unpack :: Derivation Constant -> (String, [Input Form]) + unpack (Refl _) = ("reflexivity", []) + unpack (Symm p) = ("symmetry", [deriv p]) + unpack (Trans p q) = ("transitivity", [deriv p, deriv q]) + unpack (Cong _ ps) = ("congruence", [deriv p | p <- ps, let t :=: u = equation (certify p), t /= u]) + unpack (UseAxiom Axiom{..} _) = + ("substitution", [fromJust (Map.lookup axiom_number axiom_proofs)]) + unpack (UseLemma lemma _) = + ("substitution", [fromJust (Map.lookup lemma lemma_proofs)]) 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. diff --git a/tests/ROB027-1-pretty.p b/tests/ROB027-1-pretty.p new file mode 100644 index 0000000..9e3f315 --- /dev/null +++ b/tests/ROB027-1-pretty.p @@ -0,0 +1,56 @@ +%-------------------------------------------------------------------------- +% 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, + ( '+'(X,Y) = '+'(Y,X) )). + +cnf(associativity_of_add,axiom, + ( '+'('+'(X,Y),Z) = '+'(X,'+'(Y,Z)) )). + +cnf(robbins_axiom,axiom, + ( '-'('+'('-'('+'(X,Y)),'-'('+'(X,'-'(Y))))) = X )). + +%-------------------------------------------------------------------------- +%-------------------------------------------------------------------------- +cnf(double_negation,hypothesis, + ( '-'('-'(c)) = c )). + +cnf(prove_huntingtons_axiom,negated_conjecture, + '+'('-'('+'(a,'-'(b))),'-'('+'('-'(a),'-'(b)))) != b). + +%-------------------------------------------------------------------------- +%----Definition of g +cnf(sos04,axiom,( + g(A) = '-'('+'(A,'-'(A))) )). + +%----Definition of h +cnf(sos05,axiom,( + h(A) = '+'(A,'+'(A,'+'(A,'-'('+'(A,'-'(A)))))))). diff --git a/tests/ROB027-1.p b/tests/ROB027-1.p index 835fa1f..4f8575a 100644 --- a/tests/ROB027-1.p +++ b/tests/ROB027-1.p @@ -53,4 +53,4 @@ cnf(sos04,axiom,( %----Definition of h cnf(sos05,axiom,( - h(A) = add(A,add(A,add(A,g(A)))) )). + h(A) = add(A,add(A,add(A,negate(add(A,negate(A)))))))). diff --git a/tests/append-rev-ascii.p b/tests/append-rev-ascii.p new file mode 100644 index 0000000..2a46154 --- /dev/null +++ b/tests/append-rev-ascii.p @@ -0,0 +1,4 @@ +fof(rev_rev, axiom, ![X]: rev(rev(X))=X). +fof(app_assoc, axiom, ![X, Y, Z]: '++'(X, '++'(Y, Z))='++'('++'(X, Y), Z)). +fof(rev_app, axiom, ![X, Y]: '++'(rev(X), rev(Y))=rev('++'(Y, X))). +fof(conjecture, conjecture, '++'(a, rev(b))=rev('++'(b, rev(a)))). diff --git a/tests/append-rev.p b/tests/append-rev.p index a3ba312..d7d4b2b 100644 --- a/tests/append-rev.p +++ b/tests/append-rev.p @@ -1,4 +1,4 @@ cnf(rev_rev, axiom, rev(rev(X)) = X). cnf(app_assoc, axiom, X ++ (Y ++ Z) = (X ++ Y) ++ Z). cnf(rev_app, axiom, rev(X) ++ rev(Y) = rev(Y ++ X)). -cnf(conjecture, conjecture, a ++ rev(b) = rev(b ++ rev(a))). +fof(conjecture, conjecture, ![A,B]: A ++ rev(B) = rev(B ++ rev(A))). diff --git a/tests/factor.p b/tests/factor.p index 0989c34..54d1ab3 100644 --- a/tests/factor.p +++ b/tests/factor.p @@ -1,50 +1,44 @@ % Axioms about arithmetic. -cnf('commutativity of +', axiom, +cnf('commutativity_of_plus', axiom, X + Y = Y + X). -cnf('associativity of +', axiom, +cnf('associativity_of_plus', axiom, X + (Y + Z) = (X + Y) + Z). -cnf('commutativity of *', axiom, +cnf('commutativity_of_times', axiom, X * Y = Y * X). -cnf('associativity of *', axiom, +cnf('associativity_of_times', axiom, X * (Y * Z) = (X * Y) * Z). -cnf('plus 0', axiom, +cnf('plus_zero', axiom, '0' + X = X). -cnf('times 0', axiom, +cnf('times_zero', axiom, '0' * X = '0'). -cnf('times 1', axiom, +cnf('times_one', 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). +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*(X*X)) + ((minus_six*(X*X)) + ((nine*X) + minus_four)) = ((X + + -'1')*((X + -'1') * (X + -four)))). fof(factoring, conjecture, ?[A,B,C]: ![X]: - X³ + - (-(('1'+('1'+('1'+('1'+('1'+'1')))))*(X²)) + + (X*(X*X)) + + (-(('1'+('1'+('1'+('1'+('1'+'1')))))*(X*X)) + ((('1'+('1'+('1'+('1'+('1'+('1'+('1'+('1'+'1'))))))))*X) + -('1'+('1'+('1'+'1'))))) = (X + -A)*((X + -B)*(X + -C))). diff --git a/tests/gmv.p b/tests/gmv.p new file mode 100644 index 0000000..9352ed9 --- /dev/null +++ b/tests/gmv.p @@ -0,0 +1,74 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + +cnf('Goal 1', conjecture, + x @ x = x). +cnf('Goal 2', conjecture, + (x @ y) @ z = x @ z). +cnf('Goal 3', conjecture, + x @ (y @ z) = x @ z). + +cnf('Goal 4', conjecture, + (x ∧ y) @ (z ∧ u) = (x @ z) ∧ (y @ u)). +cnf('Goal 5', conjecture, + (x ∨ y) @ (z ∨ u) = (x @ z) ∨ (y @ u)). +cnf('Goal 6', conjecture, + (x \ y) @ (z \ u) = (x @ z) \ (y @ u)). +cnf('Goal 7', conjecture, + (x / y) @ (z / u) = (x @ z) / (y @ u)). + +cnf('Goal 8', conjecture, + (x * (x \ '1')) @ '1' = x * (x \ '1')). +cnf('Goal 9', conjecture, + '1' @ (x * (x \ '1')) = '1'). +cnf('Goal 10', conjecture, + (x \ '1') @ '1' = '1'). +cnf('Goal 11', conjecture, + '1' @ (x \ '1') = x \ '1'). + +cnf('Goal 12', conjecture, + (x / (y \ x)) @ (x ∨ y) = x ∨ y). +cnf('Goal 13', conjecture, + ((x / y) \ x) @ (x ∨ y) = x ∨ y). +cnf('Goal 14', conjecture, + (x ∨ y) @ (x / (y \ x)) = x / (y \ x)). +cnf('Goal 15', conjecture, + (x ∨ y) @ ((x / y) \ x) = (x / y) \ x). diff --git a/tests/gmv1-ascii.p b/tests/gmv1-ascii.p new file mode 100644 index 0000000..b20ff25 --- /dev/null +++ b/tests/gmv1-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 1', conjecture, '@'(x, x)=x). diff --git a/tests/gmv1.p b/tests/gmv1.p new file mode 100644 index 0000000..f55a359 --- /dev/null +++ b/tests/gmv1.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + +cnf('Goal 1', conjecture, + x @ x = x). + + + diff --git a/tests/gmv10-ascii.p b/tests/gmv10-ascii.p new file mode 100644 index 0000000..b474a1a --- /dev/null +++ b/tests/gmv10-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 10', conjecture, '@'('\\'(x, '1'), '1')='1'). diff --git a/tests/gmv10.p b/tests/gmv10.p new file mode 100644 index 0000000..d2a6055 --- /dev/null +++ b/tests/gmv10.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + + +cnf('Goal 10', conjecture, + (x \ '1') @ '1' = '1'). + diff --git a/tests/gmv11-ascii.p b/tests/gmv11-ascii.p new file mode 100644 index 0000000..bf863ef --- /dev/null +++ b/tests/gmv11-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 11', conjecture, '@'('1', '\\'(x, '1'))='\\'(x, '1')). diff --git a/tests/gmv11.p b/tests/gmv11.p new file mode 100644 index 0000000..0ce5d4f --- /dev/null +++ b/tests/gmv11.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + + +cnf('Goal 11', conjecture, + '1' @ (x \ '1') = x \ '1'). + diff --git a/tests/gmv12-ascii.p b/tests/gmv12-ascii.p new file mode 100644 index 0000000..97b0f58 --- /dev/null +++ b/tests/gmv12-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 12', conjecture, '@'('/'(x, '\\'(y, x)), 'or'(x, y))='or'(x, y)). diff --git a/tests/gmv12.p b/tests/gmv12.p new file mode 100644 index 0000000..ae2ddc8 --- /dev/null +++ b/tests/gmv12.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + + + +cnf('Goal 12', conjecture, + (x / (y \ x)) @ (x ∨ y) = x ∨ y). diff --git a/tests/gmv13-ascii.p b/tests/gmv13-ascii.p new file mode 100644 index 0000000..aaf5a6e --- /dev/null +++ b/tests/gmv13-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 13', conjecture, '@'('\\'('/'(x, y), x), 'or'(x, y))='or'(x, y)). diff --git a/tests/gmv13.p b/tests/gmv13.p new file mode 100644 index 0000000..7218c8e --- /dev/null +++ b/tests/gmv13.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + + + +cnf('Goal 13', conjecture, + ((x / y) \ x) @ (x ∨ y) = x ∨ y). diff --git a/tests/gmv14-ascii.p b/tests/gmv14-ascii.p new file mode 100644 index 0000000..5037673 --- /dev/null +++ b/tests/gmv14-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 14', conjecture, '@'('or'(x, y), '/'(x, '\\'(y, x)))='/'(x, '\\'(y, x))). diff --git a/tests/gmv14.p b/tests/gmv14.p new file mode 100644 index 0000000..42fefe6 --- /dev/null +++ b/tests/gmv14.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + + + +cnf('Goal 14', conjecture, + (x ∨ y) @ (x / (y \ x)) = x / (y \ x)). diff --git a/tests/gmv15-ascii.p b/tests/gmv15-ascii.p new file mode 100644 index 0000000..13bc44d --- /dev/null +++ b/tests/gmv15-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 15', conjecture, '@'('or'(x, y), '\\'('/'(x, y), x))='\\'('/'(x, y), x)). diff --git a/tests/gmv15.p b/tests/gmv15.p new file mode 100644 index 0000000..24db2f1 --- /dev/null +++ b/tests/gmv15.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + + + +cnf('Goal 15', conjecture, + (x ∨ y) @ ((x / y) \ x) = (x / y) \ x). diff --git a/tests/gmv2-ascii.p b/tests/gmv2-ascii.p new file mode 100644 index 0000000..efcc9f3 --- /dev/null +++ b/tests/gmv2-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 2', conjecture, '@'('@'(x, y), z)='@'(x, z)). diff --git a/tests/gmv2.p b/tests/gmv2.p new file mode 100644 index 0000000..7f817a6 --- /dev/null +++ b/tests/gmv2.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + +cnf('Goal 2', conjecture, + (x @ y) @ z = x @ z). + + + diff --git a/tests/gmv3-ascii.p b/tests/gmv3-ascii.p new file mode 100644 index 0000000..0e27084 --- /dev/null +++ b/tests/gmv3-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 3', conjecture, '@'(x, '@'(y, z))='@'(x, z)). diff --git a/tests/gmv3.p b/tests/gmv3.p new file mode 100644 index 0000000..fbe1757 --- /dev/null +++ b/tests/gmv3.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + +cnf('Goal 3', conjecture, + x @ (y @ z) = x @ z). + + + diff --git a/tests/gmv4-ascii.p b/tests/gmv4-ascii.p new file mode 100644 index 0000000..fd5555f --- /dev/null +++ b/tests/gmv4-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 4', conjecture, '@'('and'(x, y), 'and'(z, u))='and'('@'(x, z), '@'(y, u))). diff --git a/tests/gmv4.p b/tests/gmv4.p new file mode 100644 index 0000000..0c17289 --- /dev/null +++ b/tests/gmv4.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + +cnf('Goal 4', conjecture, + (x ∧ y) @ (z ∧ u) = (x @ z) ∧ (y @ u)). + + diff --git a/tests/gmv5-ascii.p b/tests/gmv5-ascii.p new file mode 100644 index 0000000..eb80332 --- /dev/null +++ b/tests/gmv5-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 5', conjecture, '@'('or'(x, y), 'or'(z, u))='or'('@'(x, z), '@'(y, u))). diff --git a/tests/gmv5.p b/tests/gmv5.p new file mode 100644 index 0000000..eb5c4bb --- /dev/null +++ b/tests/gmv5.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + +cnf('Goal 5', conjecture, + (x ∨ y) @ (z ∨ u) = (x @ z) ∨ (y @ u)). + + diff --git a/tests/gmv6-ascii.p b/tests/gmv6-ascii.p new file mode 100644 index 0000000..0b42fd9 --- /dev/null +++ b/tests/gmv6-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 6', conjecture, '@'('\\'(x, y), '\\'(z, u))='\\'('@'(x, z), '@'(y, u))). diff --git a/tests/gmv6.p b/tests/gmv6.p new file mode 100644 index 0000000..69416aa --- /dev/null +++ b/tests/gmv6.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + +cnf('Goal 6', conjecture, + (x \ y) @ (z \ u) = (x @ z) \ (y @ u)). + + diff --git a/tests/gmv7-ascii.p b/tests/gmv7-ascii.p new file mode 100644 index 0000000..fd2dc98 --- /dev/null +++ b/tests/gmv7-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 7', conjecture, '@'('/'(x, y), '/'(z, u))='/'('@'(x, z), '@'(y, u))). diff --git a/tests/gmv7.p b/tests/gmv7.p new file mode 100644 index 0000000..7c1d8af --- /dev/null +++ b/tests/gmv7.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + +cnf('Goal 7', conjecture, + (x / y) @ (z / u) = (x @ z) / (y @ u)). + + diff --git a/tests/gmv8-ascii.p b/tests/gmv8-ascii.p new file mode 100644 index 0000000..4dd769b --- /dev/null +++ b/tests/gmv8-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 8', conjecture, '@'('*'(x, '\\'(x, '1')), '1')='*'(x, '\\'(x, '1'))). diff --git a/tests/gmv8.p b/tests/gmv8.p new file mode 100644 index 0000000..2759448 --- /dev/null +++ b/tests/gmv8.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + + +cnf('Goal 8', conjecture, + (x * (x \ '1')) @ '1' = x * (x \ '1')). + diff --git a/tests/gmv9-ascii.p b/tests/gmv9-ascii.p new file mode 100644 index 0000000..1af0cc7 --- /dev/null +++ b/tests/gmv9-ascii.p @@ -0,0 +1,19 @@ +fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))). +fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))). +fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X). +fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X). +fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)). +fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)). +fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X). +fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X). +fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z). +fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z). +fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y). +fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y). +fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))). +fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X). +fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X). +fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))). +fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)). +fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))). +fof('Goal 9', conjecture, '@'('1', '*'(x, '\\'(x, '1')))='1'). diff --git a/tests/gmv9.p b/tests/gmv9.p new file mode 100644 index 0000000..edfa234 --- /dev/null +++ b/tests/gmv9.p @@ -0,0 +1,46 @@ +cnf('Associativity-∧', axiom, + (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). +cnf('Associativity-∨', axiom, + (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)). +cnf('Idempotence-∧', axiom, + X ∧ X = X). +cnf('Idempotence-∨', axiom, + X ∨ X = X). +cnf('Commutativity-∧', axiom, + X ∧ Y = Y ∧ X). +cnf('Commutativity-∨', axiom, + X ∨ Y = Y ∨ X). +cnf('Absorption a', axiom, + (X ∧ Y) ∨ X = X). +cnf('Absorption b', axiom, + (X ∨ Y) ∧ X = X). + +cnf('Residual a', axiom, + (X * ((X \ Z) ∧ Y)) ∨ Z = Z). +cnf('Residual b', axiom, + ((Y ∧ (Z / X)) * X) ∨ Z = Z). +cnf('Residual c', axiom, + (X \ ((X * Y) ∨ Z)) ∧ Y = Y). +cnf('Residual d', axiom, + (((Y * X) ∨ Z) / X) ∧ Y = Y). + +cnf('Associativity-* (fusion)', axiom, + (X * Y) * Z = X * (Y * Z)). +cnf('Left monoid unit', axiom, + '1' * X = X). +cnf('Right monoid unit', axiom, + X * '1' = X). + +cnf('GMV a', axiom, + X ∨ Y = X / ((X ∨ Y) \ X)). +cnf('GMV b', axiom, + X ∨ Y = (X / (X ∨ Y)) \ X). + +cnf('Definition-@', axiom, + X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')). + + + +cnf('Goal 9', conjecture, + '1' @ (x * (x \ '1')) = '1'). + diff --git a/tests/group_plain.p b/tests/group_plain.p new file mode 100644 index 0000000..f48264e --- /dev/null +++ b/tests/group_plain.p @@ -0,0 +1,14 @@ +cnf(associativity, axiom, + plus(X,plus(Y,Z))=plus(plus(X,Y),Z)). +cnf(plus_zero, axiom, + plus(zero, X) = X). +cnf(plus_zero, axiom, + plus(X, zero) = X). +cnf(minus_left, axiom, + plus(neg(X),X) = zero). +cnf(minus_right, axiom, + plus(X,neg(X)) = zero). +cnf(assumption, assumption, + plus(a, b) = a). +cnf(goal, conjecture, + b = zero). diff --git a/tests/veroff-short.p b/tests/veroff-short.p new file mode 100644 index 0000000..8c0b66a --- /dev/null +++ b/tests/veroff-short.p @@ -0,0 +1,11 @@ +cnf(majority, axiom, + f(X,X,Y) = X). +cnf('2a', axiom, + f(X,Y,Z) = f(Z,X,Y)). +cnf('2b', axiom, + f(X,Y,Z) = f(X,Z,Y)). +cnf(associativity, axiom, + f(f(X,W,Y),W,Z) = f(X,W,f(Y,W,Z))). + +cnf(dist_long, conjecture, + f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w))). @@ -1,5 +1,5 @@ name: twee -version: 2.3 +version: 2.3.1 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3 @@ -52,7 +52,7 @@ executable twee other-modules: SequentialMain default-language: Haskell2010 build-depends: base < 5, - twee-lib == 2.3, + twee-lib == 2.3.1, containers, pretty, split, |