From 228b2032f701c8250e295001dfcf58d3570602dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sat, 2 Nov 2019 05:06:55 +0100 Subject: [PATCH] Make anthem axiomatization more consistent --- src/tptp_preamble_anthem_axioms.tptp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/tptp_preamble_anthem_axioms.tptp b/src/tptp_preamble_anthem_axioms.tptp index c4d0d09..cbbd058 100644 --- a/src/tptp_preamble_anthem_axioms.tptp +++ b/src/tptp_preamble_anthem_axioms.tptp @@ -1,15 +1,15 @@ -tff(axiom, axiom, ![X: object]: (p__is_integer__(X) <=> (?[Y: $int]: (X = f__integer__(Y))))). -tff(axiom, axiom, ![X: object]: (p__is_symbolic__(X) <=> (?[Y: $i]: (X = f__symbolic__(Y))))). +tff(axiom, axiom, ![X: object]: (p__is_integer__(X) <=> (?[N: $int]: (X = f__integer__(N))))). +tff(axiom, axiom, ![X1: object]: (p__is_symbolic__(X1) <=> (?[X2: $i]: (X1 = f__symbolic__(X2))))). tff(axiom, axiom, ![X: object]: ((X = c__infimum__) | p__is_integer__(X) | p__is_symbolic__(X) | (X = c__supremum__))). -tff(axiom, axiom, ![X: $int, Y: $int]: ((f__integer__(X) = f__integer__(Y)) <=> (X = Y))). -tff(axiom, axiom, ![X: $i, Y: $i]: ((f__symbolic__(X) = f__symbolic__(Y)) <=> (X = Y))). -tff(axiom, axiom, ![X1: $int, X2: $int]: (p__less_equal__(f__integer__(X1), f__integer__(X2)) <=> $lesseq(X1, X2))). +tff(axiom, axiom, ![N1: $int, N2: $int]: ((f__integer__(N1) = f__integer__(N2)) <=> (N1 = N2))). +tff(axiom, axiom, ![S1: $i, S2: $i]: ((f__symbolic__(S1) = f__symbolic__(S2)) <=> (S1 = S2))). +tff(axiom, axiom, ![N1: $int, N2: $int]: (p__less_equal__(f__integer__(N1), f__integer__(N2)) <=> $lesseq(N1, N2))). tff(axiom, axiom, ![X1: object, X2: object]: ((p__less_equal__(X1, X2) & p__less_equal__(X2, X1)) => (X1 = X2))). tff(axiom, axiom, ![X1: object, X2: object, X3: object]: ((p__less_equal__(X1, X2) & p__less_equal__(X2, X3)) => p__less_equal__(X1, X3))). tff(axiom, axiom, ![X1: object, X2: object]: (p__less_equal__(X1, X2) | p__less_equal__(X2, X1))). tff(axiom, axiom, ![X1: object, X2: object]: (p__less__(X1, X2) <=> (p__less_equal__(X1, X2) & (X1 != X2)))). tff(axiom, axiom, ![X1: object, X2: object]: (p__greater_equal__(X1, X2) <=> p__less_equal__(X2, X1))). tff(axiom, axiom, ![X1: object, X2: object]: (p__greater__(X1, X2) <=> (p__less_equal__(X2, X1) & (X1 != X2)))). -tff(axiom, axiom, ![X: $int]: p__less__(c__infimum__, f__integer__(X))). -tff(axiom, axiom, ![X1: $int, X2: $i]: p__less__(f__integer__(X1), f__symbolic__(X2))). -tff(axiom, axiom, ![X: $i]: p__less__(f__symbolic__(X), c__supremum__)). +tff(axiom, axiom, ![N: $int]: p__less__(c__infimum__, f__integer__(N))). +tff(axiom, axiom, ![N: $int, S: $i]: p__less__(f__integer__(N), f__symbolic__(S))). +tff(axiom, axiom, ![S: $i]: p__less__(f__symbolic__(S), c__supremum__)).