| 707e41f | Dominik Kirst | 18 April 2020, 09:27:26 UTC | fixed typo in my hometown | 18 April 2020, 09:27:26 UTC |
| f5b1a44 | Dominik Kirst | 17 April 2020, 11:02:46 UTC | nesting level only on 2 now | 17 April 2020, 11:02:46 UTC |
| 0c4c5f8 | Dominik Kirst | 17 April 2020, 10:46:05 UTC | improved coqdoc | 17 April 2020, 10:46:05 UTC |
| 3924a30 | Dominique Larchey-Wendling | 08 April 2020, 20:09:30 UTC | simplified the construction of the relational model based on HFS sets to make it more coherent with the explanation in the paper. | 08 April 2020, 20:09:30 UTC |
| 2524a2e | Dominique Larchey-Wendling | 03 April 2020, 12:40:59 UTC | update CeCILL License to 2.1 | 03 April 2020, 12:40:59 UTC |
| 529b151 | Dominique Larchey-Wendling | 11 March 2020, 13:51:01 UTC | corrected summary.v to account for Reviewer 3 (thm 37 and thm 38 swapped) | 11 March 2020, 13:51:01 UTC |
| 5de5024 | Dominique Larchey-Wendling | 26 January 2020, 18:39:02 UTC | update README | 26 January 2020, 18:39:02 UTC |
| 862bbca | Dominique Larchey-Wendling | 26 January 2020, 18:36:04 UTC | updated Readme | 26 January 2020, 18:36:04 UTC |
| b9bf7f6 | Dominique Larchey-Wendling | 26 January 2020, 17:34:22 UTC | commented out two Checks | 26 January 2020, 17:34:22 UTC |
| 6a569bd | Dominique Larchey-Wendling | 25 January 2020, 23:08:14 UTC | updated Readme | 25 January 2020, 23:08:14 UTC |
| fa2512c | Dominique Larchey-Wendling | 25 January 2020, 22:58:36 UTC | filled the TOC which documents every file in TRAKH/*.v | 25 January 2020, 22:58:36 UTC |
| 81a4af4 | Dominique Larchey-Wendling | 23 January 2020, 21:54:52 UTC | working out a better TOC | 23 January 2020, 21:54:52 UTC |
| 37760fe | Dominique Larchey-Wendling | 23 January 2020, 21:13:55 UTC | Local Defs instead of Let to allow for hyperlinks to work in CoqDoc | 23 January 2020, 21:13:55 UTC |
| 1ca41d8 | Dominique Larchey-Wendling | 23 January 2020, 20:31:06 UTC | removed unneeded files | 23 January 2020, 20:31:06 UTC |
| e41cf3e | Dominique Larchey-Wendling | 23 January 2020, 20:28:13 UTC | added : core after every Hint because of 8.10.1 warnings | 23 January 2020, 20:28:13 UTC |
| 96f44f4 | Dominique Larchey-Wendling | 23 January 2020, 19:28:43 UTC | a new README | 23 January 2020, 19:28:43 UTC |
| 32bb222 | Dominique Larchey-Wendling | 23 January 2020, 15:25:06 UTC | name change for coqlinks | 23 January 2020, 15:25:06 UTC |
| ab62cfb | Dominique Larchey-Wendling | 22 January 2020, 23:27:44 UTC | some more comments and links related changes | 22 January 2020, 23:27:44 UTC |
| b3fb500 | Dominique Larchey-Wendling | 22 January 2020, 22:55:08 UTC | removing Σ in names for coqlinks !!! | 22 January 2020, 22:55:08 UTC |
| 657ca94 | Dominique Larchey-Wendling | 22 January 2020, 22:42:45 UTC | some comments cleanup wrt _ | 22 January 2020, 22:42:45 UTC |
| 7cfd84e | dominik-kirst | 22 January 2020, 20:40:43 UTC | added header and footer files | 22 January 2020, 20:40:43 UTC |
| 7dd0021 | Dominique Larchey-Wendling | 22 January 2020, 18:28:19 UTC | some updates for the appendix of the paper | 22 January 2020, 18:28:19 UTC |
| 8897308 | Dominique Larchey-Wendling | 22 January 2020, 14:42:15 UTC | Merge branch 'trakhtenbrot_ijcar' of github.com:uds-psl/coq-library-undecidability into trakhtenbrot_ijcar | 22 January 2020, 14:42:15 UTC |
| f1fde55 | Dominique Larchey-Wendling | 22 January 2020, 14:42:01 UTC | small ordering change | 22 January 2020, 14:42:01 UTC |
| 50add36 | Dominique Larchey-Wendling | 22 January 2020, 11:06:38 UTC | completed summary with BPCP <-> BPCP_problem | 22 January 2020, 11:06:38 UTC |
| da96922 | Dominique Larchey-Wendling | 22 January 2020, 10:59:36 UTC | proved Fact 5 and removed ref. to Prelims.v in Reduction.v because Prelims.v had a strange side effect wrt to implicit arguments in fo_terms.v (even thought it was not imported directly by fo_terms.v) | 22 January 2020, 10:59:36 UTC |
| a3842ab | dominik-kirst | 22 January 2020, 05:19:37 UTC | escaping underscores in comments | 22 January 2020, 05:19:37 UTC |
| d1b999c | dominik-kirst | 22 January 2020, 03:40:42 UTC | makefiles for website generation | 22 January 2020, 03:40:42 UTC |
| 24b2614 | Dominique Larchey-Wendling | 21 January 2020, 16:59:03 UTC | forgot to remove that spare repo TRAKH*/saved that contained no longer used Coq code | 21 January 2020, 16:59:03 UTC |
| 65f1626 | Dominique Larchey-Wendling | 21 January 2020, 16:43:03 UTC | the last two unused | 21 January 2020, 16:43:03 UTC |
| 8802abb | Dominique Larchey-Wendling | 21 January 2020, 16:42:08 UTC | more prunning of unused code | 21 January 2020, 16:42:08 UTC |
| 6e4d674 | Dominique Larchey-Wendling | 21 January 2020, 14:44:03 UTC | filling the summary file with all the Check & Print corresponding to the IJCAR paper | 21 January 2020, 14:44:03 UTC |
| 90d65e1 | Dominique Larchey-Wendling | 21 January 2020, 13:17:24 UTC | first commit in this branch removing all unnecessary stuff for UNDEC lib | 21 January 2020, 13:17:24 UTC |
| 5c7fdc8 | Dominique Larchey-Wendling | 21 January 2020, 10:46:19 UTC | reduced the dependencies over the whole lib ... now compile time is less than 1 minute the only needed external libs are in Shared/Libs/DLW/* little in PCP/* and Problems/[Reduction.v,PCP.v] and of course much of TRAKHTENBROT/* | 21 January 2020, 10:46:19 UTC |
| e95849a | Dominique Larchey-Wendling | 21 January 2020, 10:05:53 UTC | moved the def of discrete in decidable.v | 21 January 2020, 10:05:53 UTC |
| 8cd60f0 | Dominique Larchey-Wendling | 20 January 2020, 15:00:47 UTC | small cleanups and statements that were missing | 20 January 2020, 15:00:47 UTC |
| f7db443 | Dominique Larchey-Wendling | 20 January 2020, 08:18:43 UTC | a simpler summary file | 20 January 2020, 08:18:43 UTC |
| 20d7ac3 | Dominique Larchey-Wendling | 19 January 2020, 10:13:31 UTC | added a mapping for formulas void of symbols | 19 January 2020, 10:13:31 UTC |
| 062c0d9 | Dominique Larchey-Wendling | 13 January 2020, 14:16:20 UTC | converted to INFORMATIVE reductions throughout ALL THE LIBRARY !! | 13 January 2020, 14:16:20 UTC |
| aedbd1a | Dominique Larchey-Wendling | 13 January 2020, 10:25:54 UTC | improved the proof of decidability for degenerate case where relations are of arity zero ... no constraint on symbols is needed because there are no symbols in formulas in this case. Also reworked the structure a bit | 13 January 2020, 10:25:54 UTC |
| f4a8ed6 | Dominique Larchey-Wendling | 11 January 2020, 00:12:23 UTC | cleanup and enumeration for vectors and lists | 11 January 2020, 00:12:23 UTC |
| 06129f3 | Dominique Larchey-Wendling | 10 January 2020, 23:23:35 UTC | upgraded enumerability results to strong enumerability | 10 January 2020, 23:23:35 UTC |
| e001ca3 | Dominique Larchey-Wendling | 10 January 2020, 22:52:10 UTC | added the enumeration of FO formulas using height to enumerate progessivelly using a measure | 10 January 2020, 22:52:10 UTC |
| 78f6acf | Dominique Larchey-Wendling | 10 January 2020, 13:03:39 UTC | added enumerability of FSAT for discrete signatures | 10 January 2020, 13:03:39 UTC |
| 9b219e8 | Dominique Larchey-Wendling | 09 January 2020, 22:49:03 UTC | all the classification is now summerized in summary.v | 09 January 2020, 22:49:03 UTC |
| ccca100 | Dominique Larchey-Wendling | 09 January 2020, 21:15:26 UTC | all the decidable cases are in | 09 January 2020, 21:15:26 UTC |
| ab29c21 | Dominique Larchey-Wendling | 09 January 2020, 20:20:32 UTC | added decidability of FSAT for FULL MONADIC FOL, ie with functions and relations of arity <= 1 (over a discrete signature) | 09 January 2020, 20:20:32 UTC |
| 6a88a98 | Dominique Larchey-Wendling | 09 January 2020, 15:22:52 UTC | added signature transport from discrete to (pos n) (pos m) to get decidability | 09 January 2020, 15:22:52 UTC |
| 91704a1 | Dominique Larchey-Wendling | 09 January 2020, 11:13:19 UTC | remove propositional constants from monadic signatures | 09 January 2020, 11:13:19 UTC |
| 8a767ca | Dominique Larchey-Wendling | 08 January 2020, 23:30:33 UTC | implemented the elimination of function symbols for full monadic FOL | 08 January 2020, 23:30:33 UTC |
| 3c30028 | Dominique Larchey-Wendling | 08 January 2020, 08:54:41 UTC | a better elimination of r(s::w) into pos0(w) | 08 January 2020, 08:54:41 UTC |
| 70aa4d0 | Dominique Larchey-Wendling | 08 January 2020, 01:28:26 UTC | implimenting the elimination of unary functions symbols according to "The Classical Decision Problem" pp 251 | 08 January 2020, 01:28:26 UTC |
| 56482df | Dominique Larchey-Wendling | 03 January 2020, 20:37:00 UTC | reduction Σ=(ø,{R_2}) -> Σ=({f_n},{P_1}) with n >= 2 | 03 January 2020, 20:37:00 UTC |
| 0cd7558 | Dominique Larchey-Wendling | 02 January 2020, 21:18:29 UTC | forgot the file !!! | 02 January 2020, 21:18:29 UTC |
| d898cae | Dominique Larchey-Wendling | 02 January 2020, 21:12:09 UTC | proved that Σ21 = ({f_2},{P_1}) has undecidable FSAT hence we have all undecidable cases ... remains to show that unary funs + unary rels are decidable | 02 January 2020, 21:12:09 UTC |
| e8467a1 | Dominique Larchey-Wendling | 29 December 2019, 10:20:49 UTC | proved the decidability of monadic FOL with n unary rels and no function symbols | 29 December 2019, 10:20:49 UTC |
| b4cb755 | Dominique Larchey-Wendling | 27 December 2019, 18:32:48 UTC | decidability of FSAT for monadic FOL with n relations provided decidability of FSAT when the underlying type is fixed !! | 27 December 2019, 18:32:48 UTC |
| cec439d | Dominique Larchey-Wendling | 27 December 2019, 16:13:33 UTC | tool for the decidability of monadic FOL, ie a bound on the size of base type for FO models. | 27 December 2019, 16:13:33 UTC |
| 7a6e6c4 | Dominique Larchey-Wendling | 24 December 2019, 10:50:42 UTC | a new reduction DISCRETE_TO_BINARY_ALT : FSAT Σ ⪯ FSAT (Σrel 2) using the existing chain but I needed to switch to informative reductions (a bit stronger results) and equivalence between the Library's def of BPCP and ours which are a bit different formally | 24 December 2019, 10:50:42 UTC |
| 74b0897 | Dominique Larchey-Wendling | 23 December 2019, 13:16:23 UTC | another proof that Σ ~~> Σ2 in the discrete case only by restricting the signature to a finitary signature and then applying the previous ... | 23 December 2019, 13:16:23 UTC |
| 1098508 | Dominique Larchey-Wendling | 20 December 2019, 20:00:12 UTC | cleanup automation | 20 December 2019, 20:00:12 UTC |
| f90ffd1 | Dominique Larchey-Wendling | 20 December 2019, 17:37:52 UTC | the redution Sig -> Sig2 is now in reductions.v | 20 December 2019, 17:37:52 UTC |
| 3165b5f | Dominique Larchey-Wendling | 20 December 2019, 12:42:35 UTC | finished the reduction Σ ~~> Σ2 in Sig_Sig2.v now I just need to import into reductions.v | 20 December 2019, 12:42:35 UTC |
| 9177c7d | Dominique Larchey-Wendling | 19 December 2019, 23:28:18 UTC | nearly finished the reduction Σ -> Σ2 too little but perhaps annoying "admits" regarding functionality and totality in the hfs model. Perhaps the axiomatization of is not strong enough ... | 19 December 2019, 23:28:18 UTC |
| b0622e1 | Dominique Larchey-Wendling | 19 December 2019, 20:56:51 UTC | finished the completeness of the reduction Σ ~~> Σ2 with just the assumption of discreteness of Σ remaining is the soundness by the semantic part is already done in rels_hfs.v | 19 December 2019, 20:56:51 UTC |
| 8ddf702 | Dominique Larchey-Wendling | 17 December 2019, 19:08:08 UTC | reworked the reductions to factor out the reduction finitary Σ --> Σ2 | 17 December 2019, 19:08:08 UTC |
| f31342a | Dominique Larchey-Wendling | 17 December 2019, 14:43:06 UTC | damn variables names ;-) | 17 December 2019, 14:43:06 UTC |
| 3e8f496 | Dominique Larchey-Wendling | 17 December 2019, 14:33:53 UTC | this one compiles for me | 17 December 2019, 14:33:53 UTC |
| 81f29bc | Dominique Larchey-Wendling | 16 December 2019, 14:14:22 UTC | added the reduction Σn --> Σ2 that @DK asked for (so long ...) as a variant/generalization of the Σ3 --> Σ2 reduction | 16 December 2019, 14:14:22 UTC |
| 375ec87 | Dominique Larchey-Wendling | 16 December 2019, 09:00:06 UTC | added tuples to membership.v in preparation for Σn -> Σ2 | 16 December 2019, 09:00:06 UTC |
| e8cfa97 | Dominique Larchey-Wendling | 13 December 2019, 23:26:35 UTC | some changes to be in coherence with the explanations in the paper | 13 December 2019, 23:26:35 UTC |
| 655a3ce | Dominique Larchey-Wendling | 12 December 2019, 13:26:30 UTC | updated reduction removing symbols to make the reduced signature like in the paper ie {=} + syms + rels instead of syms + {=} + rels | 12 December 2019, 13:26:30 UTC |
| 1880fe4 | Dominique Larchey-Wendling | 12 December 2019, 12:58:07 UTC | update De Bruijn extension notations to be coherent with the paper | 12 December 2019, 12:58:07 UTC |
| 15a36a4 | Dominique Larchey-Wendling | 08 December 2019, 18:56:22 UTC | strenghtened the quotient construction so that we only assume enumerability of equivalence classes | 08 December 2019, 18:56:22 UTC |
| ee6077a | Dominique Larchey-Wendling | 08 December 2019, 17:11:32 UTC | generalized the quotient constructino to arbitrary enumerable types with a decidable equivalence ... it might be possible to weaken it to enumerability of equivalence classes | 08 December 2019, 17:11:32 UTC |
| 7f86311 | Dominique Larchey-Wendling | 08 December 2019, 12:55:45 UTC | added quotient of decidable equivalence over nat giving an enumerable and discrete type and the class and repr functions | 08 December 2019, 12:55:45 UTC |
| 6d57c4d | Dominique Larchey-Wendling | 07 December 2019, 08:33:44 UTC | cleanup | 07 December 2019, 08:33:44 UTC |
| addcc91 | Dominique Larchey-Wendling | 07 December 2019, 08:23:51 UTC | simplified reductions.v so that intermediate steps are always FSAT in finite and decidable SAT over some signature replaced former intermediated steps with corollaries that somehow hide FIN & DEC & DISCRETE or FIN & DEC & INTERPRETED to better match what is going to be explained in the paper | 07 December 2019, 08:23:51 UTC |
| 0c2b9cf | Dominique Larchey-Wendling | 06 December 2019, 14:15:26 UTC | reordered the statements in reductions.v to respect the order of the reduction chain, putting the two utility reductions in front | 06 December 2019, 14:15:26 UTC |
| b108245 | Dominique Larchey-Wendling | 06 December 2019, 13:53:01 UTC | Split Sig_noeq.v in half separating the encoding of the congruence in FOL | 06 December 2019, 13:53:01 UTC |
| 76eae88 | Dominique Larchey-Wendling | 06 December 2019, 11:42:37 UTC | cleanup in Sig_noeq.v | 06 December 2019, 11:42:37 UTC |
| ed467ba | Dominique Larchey-Wendling | 06 December 2019, 10:43:08 UTC | removed the use of the model discretizer in Sig_noeq.v | 06 December 2019, 10:43:08 UTC |
| def226b | Dominique Larchey-Wendling | 05 December 2019, 21:14:23 UTC | some more cleanup | 05 December 2019, 21:14:23 UTC |
| 9a8079e | Dominique Larchey-Wendling | 05 December 2019, 21:01:44 UTC | MAJOR cleanup and removal of unnecessary code | 05 December 2019, 21:01:44 UTC |
| 494dd93 | Dominique Larchey-Wendling | 05 December 2019, 18:31:53 UTC | converted to new fo_term notations | 05 December 2019, 18:31:53 UTC |
| 1a3b573 | Dominique Larchey-Wendling | 05 December 2019, 15:27:51 UTC | cleanup some notations | 05 December 2019, 15:27:51 UTC |
| 45369d1 | Dominique Larchey-Wendling | 05 December 2019, 14:06:57 UTC | restructured with a .v for fo_signatures and reworked the proof of BCPC -> finite signature so that the target is finite&decidable&interpret SAT (proof is simpler) | 05 December 2019, 14:06:57 UTC |
| a03aa60 | Dominique Larchey-Wendling | 05 December 2019, 08:07:49 UTC | added the elimination of constant symbols assuming only discreteness of the type of symbols | 05 December 2019, 08:07:49 UTC |
| fb44241 | Dominique Larchey-Wendling | 04 December 2019, 17:58:36 UTC | adding Fixpoint definitions for fo_term if prefered over ... | 04 December 2019, 17:58:36 UTC |
| c45ae56 | Dominique Larchey-Wendling | 04 December 2019, 14:08:35 UTC | started removing constants... | 04 December 2019, 14:08:35 UTC |
| 208036b | Dominique Larchey-Wendling | 03 December 2019, 23:13:10 UTC | cleanup the code in the compression of arity n --> 1+n and constants | 03 December 2019, 23:13:10 UTC |
| 306c9b5 | Dominique Larchey-Wendling | 03 December 2019, 22:36:51 UTC | imported Domink's reduction from uniform arity n -> to one n+1 and constants | 03 December 2019, 22:36:51 UTC |
| 49079a2 | Dominique Larchey-Wendling | 03 December 2019, 12:07:36 UTC | forget to update the statement of the hole | 03 December 2019, 12:07:36 UTC |
| c40ac2b | Dominique Larchey-Wendling | 03 December 2019, 11:59:10 UTC | reduction to uniform arity (= n) of relations (when the original arities are <= n) | 03 December 2019, 11:59:10 UTC |
| d73c3cf | Dominique Larchey-Wendling | 02 December 2019, 14:40:57 UTC | the proof of the Full Trakhtenbrot theorem with the only hole remaining being the reduction from finitely many relation symbols to just one of strictly greater arity (to be filled by Dominik) | 02 December 2019, 14:40:57 UTC |
| f5d794a | Dominique Larchey-Wendling | 02 December 2019, 14:10:19 UTC | Modified Sig_noeq.v to handle implicit interpreted identity worked out mostly fine | 02 December 2019, 14:10:19 UTC |
| 681c502 | Dominique Larchey-Wendling | 02 December 2019, 10:54:31 UTC | reduction for finite interpreted SAT to (uninterpreted) finite SAT for a signature with an explicited equality symbol | 02 December 2019, 10:54:31 UTC |
| 184042d | Dominique Larchey-Wendling | 01 December 2019, 08:07:07 UTC | commented out TRAKHTENBROT/SigBPCP_Sig32.v which is a failed attempt now decomposed into 1) first remove the symbols 2) compress to a ternary relation | 01 December 2019, 08:07:07 UTC |
| 464d478 | Dominique Larchey-Wendling | 01 December 2019, 08:02:13 UTC | finished the removal of symbols for arbitrary signatures with finitely many term symbols or else discreteness of the the type of term symbols | 01 December 2019, 08:02:13 UTC |
| 06b1cb3 | Dominique Larchey-Wendling | 30 November 2019, 14:46:44 UTC | started the removal of function symbols ... I have the formula map with soundness ... completeness remains | 30 November 2019, 14:46:44 UTC |
