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.

News

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

Features

• Usage of definitions.
• Type checking.
• Break down your proof in several subproofs.
• Structural rules will be generated as needed automatically (except cut rules of course).
• Usage of meta terms and meta formulas in proofs.
• Paramodulation for handling equality.
• Proof search for propositional parts, i.e. after all necessary quantifier rules have been applied the proof can be completed automatically.
• Recursive functions, predicates and proofs.

Requirements

• libxml2 (at least version 2.6.7)

Download

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.

Example

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
  proves
    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:

Documentation

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

• hlk Synopsis:

  Usage: hlk [options] <filename> <proof-name>
  
  Options:
    --version          print the version of hlk.
    -o <filename>      output file (default /dev/stdout).
    --flat             output flat proof.
    --ceres            output ceres input.
    --slk              skeleton lk output.
    --latex            output proof(s) as LaTeX source.
    --sim-undef        simulate undef predicate rules.
    --axioms[=<file>]  will output the initial sequents to file,
                       default ist /dev/stderr.

• A simple syntax description of HLK.
• The output calculus definition.
• The XML DTD of the output: proofdatabase.dtd and

Links

• Proof Tool is a viewer for LK proofs.
• CERES is a tool for automated proof analysis. HLK proofs compiled with the --ceres option can be used as input.

Contact

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