|
|
d00a2d7816
|
Typos, typos everywhere !
|
2023-08-16 19:30:18 +02:00 |
|
|
|
f20fca8392
|
Added Conclusion
|
2023-08-16 15:57:53 +02:00 |
|
|
|
66490abfb8
|
Continued report ....
|
2023-08-16 13:24:55 +02:00 |
|
|
|
360dd1823c
|
Advance on the report
|
2023-08-06 23:52:05 +02:00 |
|
|
|
841f6e96f1
|
Added automated way to extract latex from lagda files
|
2023-08-05 20:33:25 +02:00 |
|
|
|
eb80453ef2
|
Added completeness for FFOL
|
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
|
2023-08-04 16:12:18 +02:00 |
|
|
|
9be53b4f7f
|
Tried to add a completeness proof for zol
|
2023-08-03 20:43:31 +02:00 |
|
|
|
b93ce31ab3
|
Added IFOL algebra and initial and morphism and initiality proof
|
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
|
2023-08-02 23:55:25 +02:00 |
|
|
|
d70739091e
|
Continued report about Transport Hell
|
2023-08-01 18:17:18 +02:00 |
|
Ambrus Kaposi
|
2728c60633
|
put Subp in Prop
|
2023-08-01 14:19:49 +02:00 |
|
Ambrus Kaposi
|
a582f2555b
|
naming
|
2023-08-01 14:19:28 +02:00 |
|
|
|
2956b62cc1
|
Advances report, reordered some equations
|
2023-08-01 13:38:40 +02:00 |
|
|
|
e9eedbff2d
|
Added Agda code in latex, plus beginning of an introduction
|
2023-07-30 19:07:51 +02:00 |
|
|
|
357e2a087d
|
Started to write the report, created toc and files
|
2023-07-26 17:39:02 +02:00 |
|
|
|
7d03f4d854
|
Started adding the initial morphism
|
2023-07-26 15:18:25 +02:00 |
|
|
|
1d4cda091e
|
Trying Presheaf model
|
2023-07-25 15:46:40 +02:00 |
|
|
|
91d7fd127d
|
Syntax is now clean (most of it)
|
2023-07-21 15:45:31 +02:00 |
|
|
|
11a6742677
|
More tiding up
|
2023-07-20 17:35:50 +02:00 |
|
|
|
6829fe86c7
|
Started tidying up the syntax
|
2023-07-20 15:48:47 +02:00 |
|
|
|
1dc1826f49
|
Changes files names, updated Readme
|
2023-07-20 11:55:25 +02:00 |
|
|
|
a2e7689f58
|
Merge branch 'first-order'
|
2023-07-20 11:04:23 +02:00 |
|
|
|
2534ebf85e
|
Removed the Kripke model
|
2023-07-20 11:03:52 +02:00 |
|
|
|
fbf699b63e
|
Started adding completeness
|
2023-07-19 19:54:33 +02:00 |
|
|
|
824a10d5d2
|
I FINALLY HAVE A SYNTAX !!!!
|
2023-07-19 16:49:48 +02:00 |
|
|
|
a897865253
|
Added Agda new version, some progress
|
2023-07-14 16:22:05 +02:00 |
|
|
|
3c5be4ffb4
|
A bit stuck in some transport hell.
|
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)
|
2023-07-06 14:40:18 +02:00 |
|
|
|
6cfec33ff4
|
Continued the proofs, will try to make a simpler account of proof substitution
|
2023-06-29 19:15:47 +02:00 |
|
|
|
6fcaabc4db
|
Simplified the notation, working this time
|
2023-06-27 16:08:36 +02:00 |
|
|
|
8c1e71947a
|
Wrote syntax for terms, some examples commented out
|
2023-06-26 17:33:04 +02:00 |
|
|
|
bff7e48a12
|
Merge remote-tracking branch 'origin/master'
|
2023-06-22 18:58:16 +02:00 |
|
|
|
29ee842db1
|
Added some examples, but they need some lemmas using subst a lot
|
2023-06-22 18:55:16 +02:00 |
|
Thorsten Altenkirch
|
a85b9d7ad8
|
minor
|
2023-06-22 17:25:38 +02:00 |
|
Thorsten Altenkirch
|
7cf08241b4
|
added fol-subst
|
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
|
2023-06-20 17:52:07 +02:00 |
|
Thorsten Altenkirch
|
309ba6ab70
|
added examples
|
2023-06-20 15:36:18 +02:00 |
|
Thorsten Altenkirch
|
bd99520e35
|
simplified fol using l
|
2023-06-20 14:59:48 +02:00 |
|
Thorsten Altenkirch
|
00fd305f5f
|
my fol
|
2023-06-20 12:35:49 +02:00 |
|
|
|
ab7e77e833
|
Second steps, but i guess there is a problem
|
2023-06-15 12:14:35 +02:00 |
|
|
|
a2fc828d8f
|
Firsts step to an initial model
|
2023-06-14 17:00:42 +02:00 |
|
|
|
2aca2ed0ce
|
Don't comment code out when you are using git
|
2023-06-13 18:52:54 +02:00 |
|
|
|
bcff4c47e6
|
Added Kripke model for first order
|
2023-06-13 18:43:20 +02:00 |
|
|
|
a2c3882c7e
|
Completed Tarski model for finitary first order logic.
|
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
|
2023-06-09 17:34:09 +02:00 |
|
|
|
d3cf3cd0e6
|
Fixed module names as file names had changed.
|
2023-06-02 17:45:13 +02:00 |
|
|
|
c8cc4b9f54
|
Reverted to previous status and re-write logic with dumb forall -> Infinitary Logic
|
2023-06-02 17:06:40 +02:00 |
|
|
|
7ff06d3d07
|
Tried to add First order logic and First order Kripke. Some misconceptions ...
|
2023-06-02 14:37:08 +02:00 |
|
|
|
f7258e4074
|
Merge branch 'master' into first-order
|
2023-06-01 15:02:51 +02:00 |
|
