## 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.

- 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.

- libxml2 (at least version 2.6.7)

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

By calling

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

- 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.

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