TU Logo

Handy LK Homepage

Handy LK (HLK shortly) is a language for writing down complex Sequent Calculus (LK) derivations comfortably. You write down your HLK proofs into a text file (ASCII or UNICODE) and convert it into an XML or LaTeX file with the hlk compiler.


2011/08/29: HLK version beta 9 has been released. It fixes compilation problems with new versions of gcc.




Download beta 9 of HLK here. In order to install HLK correctly, follow the instructions in the INSTALL file which is contained in the src directory.


For our example we want to give a proof for a simple theorem:
The HLK file simple.hlk looks like this:
define variable x of type any;
define constant a of type any;
define function f of type any to any;
define atom predicate P of type any;

define proof the-proof
    P(a), all x ( P(x) impl P(f(x)) ) :- P( f(f(a)) );

  with all left
    P(a) impl P(f(a)) :- ;
  with all left
    P(f(a)) impl P(f(f(a))) :- ;

  continued auto propositional P(a), P(a) impl P(f(a)),
                               P(f(a)) impl P(f(f(a))) :-
			       P( f(f(a)) );

By calling hlk simple.hlk the-proof from the shell, the program will generate this XML code, which could be opened by the Proof Tool. It is also capable to generate LaTeX code (which needs proof.sty); for our example LaTeX will generate the following proof figure:


The language HLK as well as the compiler hlk are still under development, so documentation is very poor at this point.



If you have any questions or encountered problems with hlk, feel free to contact us: hlk |@| logic |.| at

Valid CSS! Valid XHTML 1.1 Viewable With Any Browser