From 963b4d260684bf538966f15084fc27bbb52cbfd6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Sicard-Ram=C3=ADrez?= Date: Wed, 9 Nov 2016 11:26:49 -0500 Subject: [PATCH] [ notes ] Added TPTP files on Mendelson's equality. --- notes/atps/mendelson-equality/refl.fof | 27 +++++++++++++ notes/atps/mendelson-equality/subst.fof | 52 +++++++++++++++++++++++++ notes/atps/mendelson-equality/sym.fof | 27 +++++++++++++ notes/atps/mendelson-equality/trans.fof | 27 +++++++++++++ 4 files changed, 133 insertions(+) create mode 100644 notes/atps/mendelson-equality/refl.fof create mode 100644 notes/atps/mendelson-equality/subst.fof create mode 100644 notes/atps/mendelson-equality/sym.fof create mode 100644 notes/atps/mendelson-equality/trans.fof diff --git a/notes/atps/mendelson-equality/refl.fof b/notes/atps/mendelson-equality/refl.fof new file mode 100644 index 00000000..2d3b5e96 --- /dev/null +++ b/notes/atps/mendelson-equality/refl.fof @@ -0,0 +1,27 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Reflexivity of Mendelson's equality +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% The conjecture was proved by the following ATPs: + +% E 1.9.1-001 +% Equinox 5.0alpha (2010-06-29) +% IleanCoP V1.3beta1 +% Metis 2.3 (release 201601108) +% Vampire 0.6 (revision 903) +% Z3 version 4.5.0 - 64 bit + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Mendelson's axioms (p. 154). + +% Mendelson, Elliott (2015). Introduction to Mathematical Logic. CRC +% Press, 6th edition. + +fof(s1, axiom, (! [M,N,O] : (eq(M,N) => (eq(M,O) => eq(N,O))))). +fof(s2, axiom, (! [M,N] : (eq(M,N) => eq(succ(M),succ(N))))). +fof(s5, axiom, (! [N] : eq(add(zero,N),N))). + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +fof(refl, conjecture, (! [M] : eq(M,M))). diff --git a/notes/atps/mendelson-equality/subst.fof b/notes/atps/mendelson-equality/subst.fof new file mode 100644 index 00000000..bd01b97a --- /dev/null +++ b/notes/atps/mendelson-equality/subst.fof @@ -0,0 +1,52 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Substitution of Mendelson's equality +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% The conjecture *could not be* proved by the following ATPs: + +% E 1.9.1-001 +% $ eprover --auto --cpu-limit=240 --memory-limit=Auto --tstp-format file_name + +% Equinox 5.0alpha (2010-06-29) +% $ equinox file_name + +% IleanCoP V1.3beta1 +% $ ileancop file_name + +% Metis 2.3 (release 20161108) +% $ metis --time-limit 240 file_name + +% Vampire 0.6 (revision 903) +% $ vampire_lin64 -t 240 --input_file file_name + +% Z3 version 4.5.0 - 64 bit +% $ tptp4X -fsmt2 file_name.fof > file_name.smt2 +% $ z3 file_name.smt2 + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Mendelson's axioms (p. 154). + +% Mendelson, Elliott (2015). Introduction to Mathematical Logic. CRC +% Press, 6th edition. + +fof(s1, axiom, (! [M,N,P] : (eq(M,N) => (eq(M,P) => eq(N,P))))). +fof(s2, axiom, (! [M,N] : (eq(M,N) => eq(succ(M),succ(N))))). +fof(s3, axiom, (! [N] : (not(eq(zero,succ(N)))))). +fof(s4, axiom, (! [M,N] : (eq(succ(M),succ(N)) => eq(M,N)))). +fof(s5, axiom, (! [N] : eq(add(zero,N),N))). +fof(s6, axiom, (! [M,N] : (eq(add(M,succ(N)),succ(add(M,N)))))). +fof(s7, axiom, (! [N] : eq(mult(N,zero),zero))). +fof(s8, axiom, (! [M,N] : (eq(mult(M,succ(N)),add(mult(M,N),M))))). + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% a = b, P a +% ----------------- substitution +% P b +fof(a1, axiom, eq(a,b)). +fof(a2, axiom, p(a)). + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +fof(subst, conjecture, p(b)). diff --git a/notes/atps/mendelson-equality/sym.fof b/notes/atps/mendelson-equality/sym.fof new file mode 100644 index 00000000..08d20ed0 --- /dev/null +++ b/notes/atps/mendelson-equality/sym.fof @@ -0,0 +1,27 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Symmetry of Mendelson's equality +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% The conjecture was proved by the following ATPs: + +% E 1.9.1-001 +% Equinox 5.0alpha (2010-06-29) +% IleanCoP V1.3beta1 +% Metis 2.3 (release 20161108) +% Vampire 0.6 (revision 903) +% Z3 version 4.5.0 - 64 bit + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Mendelson's axioms (p. 154). + +% Mendelson, Elliott (2015). Introduction to Mathematical Logic. CRC +% Press, 6th edition. + +fof(s1, axiom, (! [M,N,O] : (eq(M,N) => (eq(M,O) => eq(N,O))))). +fof(s2, axiom, (! [M,N] : (eq(M,N) => eq(succ(M),succ(N))))). +fof(s5, axiom, (! [N] : eq(add(zero,N),N))). + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +fof(sym, conjecture, (! [M,N] : (eq(M,N) => eq(N,M)))). diff --git a/notes/atps/mendelson-equality/trans.fof b/notes/atps/mendelson-equality/trans.fof new file mode 100644 index 00000000..e3b67394 --- /dev/null +++ b/notes/atps/mendelson-equality/trans.fof @@ -0,0 +1,27 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Transitivity of Mendelson's equality +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% The conjecture was proved by the following ATPs: + +% E 1.9.1-001 +% Equinox 5.0alpha (2010-06-29) +% IleanCoP V1.3beta1 +% Metis 2.3 (release 20161108) +% Vampire 0.6 (revision 903) +% Z3 version 4.5.0 - 64 bit + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Mendelson's axioms (p. 154). + +% Mendelson, Elliott (2015). Introduction to Mathematical Logic. CRC +% Press, 6th edition. + +fof(s1, axiom, (! [M,N,O] : (eq(M,N) => (eq(M,O) => eq(N,O))))). +fof(s2, axiom, (! [M,N] : (eq(M,N) => eq(succ(M),succ(N))))). +fof(s5, axiom, (! [N] : eq(add(zero,N),N))). + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +fof(sym, conjecture, (! [M,N,O] : ((eq(M,N) & eq(N,O)) => eq(M,O)))).