An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

Convert logical formulas and generate their syntax trees as vector images in SVG format. Structuralize pure C-N formulas, pure D-proofs, and index-based summaries of pure D-proofs into a universal representation that is based on the Standard Galactic Alphabet and digits of the Alteran language of the Stargate franchise.

Shortest known proofs of the propositional calculus theorems from Principia Mathematica, derived from Łukasiewicz (L₁)-system (CCpqCCqrCpr,CCNppp,CpCNpq)