the rational proof assistant

QBAR is an experimental automated theorem verifier/prover and proof assistant built on a simple abstract syntax language and a minimal proof kernel.

QBAR is currently an α-stage product and the terminal shell cannot be installed at the moment. For now, check out QBAR's dependent libraries (exprz and rational_deduction) or try the web shell.

See the web docs for the most up-to-date documentation.