A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation.

Tudor Jebelean

Browse the full LPAR paper archive.