Backport specification from my PhD thesis
This replaces the text of the specification and the rule list with the text in my PhD thesis.
Most importantly this adds an abstract proof checking procedure that specifies the semantic of an Altehe proof (modulo the proof rules).
Furthermore, it adapts the notation more to SMT-LIB: everything is in λ-application style ((f x) instead of f(x)) and we no longer have a distinct 
On the technical side this now requires lualatex for Unicode math.
Merge request reports
Activity
added format label
assigned to @hjsc
added 1 commit
- 2d4d0ff2 - Remove redundant simplification from `implies_simplify`
added 1 commit
- 17dd1226 - Remove redundant simplification from `implies_simplify`
On the technical side this now requires lualatex for Unicode math.
Do I understand correctly that the only need for the different build system is to write unicode for math symbols in the text? In that case it seems a bit much for the benefits.
Edited by Haniel Barbosa
There is no need to use a different build system. If one uses latexmk it's only necessary to add the option
-pdflatex=lualatex. If one compiles manually it's only necessary to change pdflatex to lualatex. Lualatex is installed by default with most latex packages. I think the benefit of having unicode math greatly outweighs these minimal changes to the build process.I see. I had to install lualatex separately but then I could compile via the makefile. I was afraid it was gonna be more complicated. I agree with you then (even though the benefit is somewhat inexistent to me :P I have an option to show the math commands as unicode in Emacs but I stopped using it a long time ago).
added 1 commit
- 78f5f4cf - Right align rule description (like it used to be)
added 1 commit
- 5de86985 - Activate Synctex when compiling the document
added 1 commit
- 61def906 - Apply small textual and typographic improvements
