Compiler Tools

I am developing tools that are useful for compiler construction. They are on a separate page. At this moment, the site contains a parser generator, a tokenizer generator, and a generator that converts specifications of recursive data types into C++ code.

Proof Checking with 3-Valued Logic

2026: I am implementing a proof checker based on a higher-order version of 3-valued logic called PHOLI (Partial Higher-Order Logic with Interfaces). It uses a 3-valued logic that I developed during 2010-2013, a new variant of natural deduction for this logic, and my tools that I developed for implementation of logic and compilers. The latest version can already check proofs, but it is still quite unpleasant, so more revisions will be needed. PHOLI is under continuous development, which necessarily implies unfinished. The code is on GitHub. PHOLI is closely related to my programming language project. The aim of this programming language was to able to quickly implement iterations of PHOLI. The project did not result in a programming language, but resulted in tools that are helpful with implementing logic. The current version of PHOLI uses Maphoon for parsing formulas, and TreeGen for creating the formula and proof data structures. Without TreeGen, it would probably be impossible to implement PHOLI. The underlying three-valued logic is quite tricky, and I found a suitable calculus only in December 2025. I am currently implementing this calculus. I hope that in the future, interactive theorem proving will become a pleasant experience. The modeling part is already nice.

Geo

Geo is a theorem prover, based on geometric resolution. The calculus is described in a joint IJCAR 2006 paper with Jia Meng, which can be downloaded from here

Geo III

Geo III is a new version of Geo, which aims to implement 3-valued logic in a theorem prover. See here.

Constraint Solving

The most critical part of Geo III is a constraint solver which is used for checking if a rule is applicable to a partial model. Since I believe that the implementation is efficient enough to be used stand-alone, it has a page of its own.