Mysaa/m1-internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Commit Graph

  • 1b5b148b2f
         Added appendix code generation master Mysaa 2023-08-28 17:43:21 +02:00
  • 127d1fbc9a
         Added a bit more bibliography Mysaa 2023-08-16 22:23:39 +02:00
  • d00a2d7816
         Typos, typos everywhere ! Mysaa 2023-08-16 19:30:18 +02:00
  • f20fca8392
         Added Conclusion Mysaa 2023-08-16 15:57:53 +02:00
  • 66490abfb8
         Continued report .... Mysaa 2023-08-16 13:24:55 +02:00
  • 360dd1823c
         Advance on the report Mysaa 2023-08-06 23:52:05 +02:00
  • 841f6e96f1
         Added automated way to extract latex from lagda files Mysaa 2023-08-05 20:33:25 +02:00
  • eb80453ef2
         Added completeness for FFOL Mysaa 2023-08-04 17:08:06 +02:00
  • a10bcd6770
         Added completeness for ZOL, and a more efficient way of putting agda in the LaTeX file Mysaa 2023-08-04 16:12:18 +02:00
  • 9be53b4f7f
         Tried to add a completeness proof for zol Mysaa 2023-08-03 20:43:31 +02:00
  • b93ce31ab3
         Added IFOL algebra and initial and morphism and initiality proof Mysaa 2023-08-03 14:47:49 +02:00
  • 370daed594
         Added algebra for ZOL and syntax and initial morphism and the proof of it being initial Mysaa 2023-08-02 23:55:25 +02:00
  • d70739091e
         Continued report about Transport Hell Mysaa 2023-08-01 18:17:18 +02:00
  • 2728c60633 put Subp in Prop Ambrus Kaposi 2023-08-01 14:19:49 +02:00
  • a582f2555b naming Ambrus Kaposi 2023-08-01 14:19:28 +02:00
  • 2956b62cc1
         Advances report, reordered some equations Mysaa 2023-08-01 13:38:40 +02:00
  • e9eedbff2d
         Added Agda code in latex, plus beginning of an introduction Mysaa 2023-07-30 19:07:51 +02:00
  • 357e2a087d
         Started to write the report, created toc and files Mysaa 2023-07-26 17:39:02 +02:00
  • 7d03f4d854
         Started adding the initial morphism Mysaa 2023-07-26 15:18:25 +02:00
  • 1d4cda091e
         Trying Presheaf model Mysaa 2023-07-25 15:46:40 +02:00
  • 91d7fd127d
         Syntax is now clean (most of it) Mysaa 2023-07-21 15:45:31 +02:00
  • 11a6742677
         More tiding up Mysaa 2023-07-20 17:35:50 +02:00
  • 6829fe86c7
         Started tidying up the syntax Mysaa 2023-07-20 15:48:47 +02:00
  • 1dc1826f49
         Changes files names, updated Readme Mysaa 2023-07-20 11:55:25 +02:00
  • a2e7689f58
         Merge branch 'first-order' Mysaa 2023-07-20 11:04:23 +02:00
  • 2534ebf85e
         Removed the Kripke model Mysaa 2023-07-20 11:03:52 +02:00
  • fbf699b63e
         Started adding completeness first-order Mysaa 2023-07-19 19:54:33 +02:00
  • 824a10d5d2
         I FINALLY HAVE A SYNTAX !!!! Mysaa 2023-07-19 16:49:48 +02:00
  • a897865253
         Added Agda new version, some progress Mysaa 2023-07-14 16:22:05 +02:00
  • 3c5be4ffb4
         A bit stuck in some transport hell. Mysaa 2023-07-13 12:13:26 +02:00
  • 3783c5ad15
         Ok, commit before removing a lot of useless code (i thought it was useful, i swear) Mysaa 2023-07-06 14:40:18 +02:00
  • 6cfec33ff4
         Continued the proofs, will try to make a simpler account of proof substitution Mysaa 2023-06-29 19:15:47 +02:00
  • 6fcaabc4db
         Simplified the notation, working this time Mysaa 2023-06-27 16:08:36 +02:00
  • 8c1e71947a
         Wrote syntax for terms, some examples commented out Mysaa 2023-06-26 17:33:04 +02:00
  • bff7e48a12
         Merge remote-tracking branch 'origin/master' Mysaa 2023-06-22 18:58:16 +02:00
  • 29ee842db1
         Added some examples, but they need some lemmas using subst a lot Mysaa 2023-06-22 18:55:16 +02:00
  • a85b9d7ad8 minor Thorsten Altenkirch 2023-06-22 17:25:38 +02:00
  • 7cf08241b4 added fol-subst Thorsten Altenkirch 2023-06-22 17:18:51 +02:00
  • 21bdad22a9
         Separated Syntax in another file to make Agda faster Added some proof examples that works for the Tarski model Rewrite (again) of the syntax, still not working Mysaa 2023-06-20 17:52:07 +02:00
  • 309ba6ab70 added examples Thorsten Altenkirch 2023-06-20 15:36:18 +02:00
  • bd99520e35 simplified fol using l Thorsten Altenkirch 2023-06-20 14:59:48 +02:00
  • 00fd305f5f my fol Thorsten Altenkirch 2023-06-20 12:35:49 +02:00
  • ab7e77e833
         Second steps, but i guess there is a problem Mysaa 2023-06-15 12:14:35 +02:00
  • a2fc828d8f
         Firsts step to an initial model Mysaa 2023-06-14 17:00:42 +02:00
  • 2aca2ed0ce
         Don't comment code out when you are using git Mysaa 2023-06-13 18:52:54 +02:00
  • bcff4c47e6
         Added Kripke model for first order Mysaa 2023-06-13 18:43:20 +02:00
  • a2c3882c7e
         Completed Tarski model for finitary first order logic. Mysaa 2023-06-13 15:17:41 +02:00
  • 841e6970e7
         Added First order logic and a simple Tarski model. For now, Terms are still a parameter Mysaa 2023-06-09 17:34:09 +02:00
  • d3cf3cd0e6
         Fixed module names as file names had changed. Mysaa 2023-06-02 17:45:13 +02:00
  • c8cc4b9f54
         Reverted to previous status and re-write logic with dumb forall -> Infinitary Logic Mysaa 2023-06-02 17:06:40 +02:00
  • 7ff06d3d07
         Tried to add First order logic and First order Kripke. Some misconceptions ... Mysaa 2023-06-02 14:37:08 +02:00
  • f7258e4074
         Merge branch 'master' into first-order Mysaa 2023-06-01 15:02:51 +02:00
  • c204c3f497
         Added ⊤⊤ Mysaa 2023-06-01 15:02:23 +02:00
  • 16917c0c44
         Started adding First order logic Mysaa 2023-06-01 14:43:12 +02:00
  • b11c60fc3d
         Removed older proofs in order to avoid having to rewrite them every time Mysaa 2023-06-01 12:30:28 +02:00
  • 01a029bc39
         Finished adding conjunction. Mysaa 2023-06-01 12:26:15 +02:00
  • e1f1ea32f3
         Merge branch 'master' into adding-conjunction Incomplete proofs of theorems with \and\and Mysaa 2023-05-31 14:13:15 +02:00
  • 28b7faac05
         Added a generalized version of the Normalization proof Mysaa 2023-05-31 13:59:33 +02:00
  • 422dcf67f0
         Started merging zero and next into a one and only proof constructor, so normal forms are now unique. Added a lot of relations on lists in order to study different kinds of morphisms Mysaa 2023-05-30 14:02:01 +02:00
  • 567b8bf9b6
         Started adding conjunction, made modification for PropositionalLogic Mysaa 2023-05-26 14:46:55 +02:00
  • 8d1df370ca
         Tidied files up, changed messy prop.agda into a beautiful Readme.agda Mysaa 2023-05-25 20:33:23 +02:00
  • 95bfde2377
         Added normalization proof in a separate file Mysaa 2023-05-25 18:44:11 +02:00
  • d1a0177d2c
         tinied up everything in enclosed files, with normalized notation Mysaa 2023-05-25 12:02:36 +02:00
  • ef0d5a51d7
         First commit, a functional proof completeness of kripke structure for propositional logic Mysaa 2023-05-23 18:27:34 +02:00