the rational proof assistant


The documentation and API is currently a work in progress. See the source code repository for more information.


QBAR uses an s-expression language to describe all of its data structures and abstract syntax. S-expressions are parenthesis-grouped strings which can be distinguished into two basic forms: atoms and groups. S-expressions are the syntax of choice for LISP dialects like Common Lisp, Clojure, Racket, and many others. QBAR expressions are slightly more general in that they intend to describe arbitrary data rather than just programs. See Rivest S-expressions which have a similar goal.

NOTE: Objects marked with ⚠️ have an unstable API.

Basic Forms

Expressions are either atoms, groups, or unspecified, in which case they are simply called exprs.

atom ⚠️

An atom is any Unicode string which uses " to wrap whitespace and ( ). Here are some examples:


      "a b c"

      f"Hello, {world}!"


      text-before-the-quote"text in the quote"text-after-the-quote

      []{}<>-are-also"atoms since we only care about ()"<-notice_we_had_to_escape"("and")"


Here's a regular expression that parses atoms:


NOTE: Currently, only whitespace literals and parenthesis are escaped in quoted strings. In the future, other escape sequences may be supported.


A group is an expression formed by bracketing with an open parenthesis (, delimiting with whitespace a set of expressions and then ending with a close parenthesis ).

( whitespace? {expr whitespace?}* )


An expr is either an atom or a group

atom | group

Important Shapes

NOTE: Shapes have the same syntax as expressions except we don't notate optional whitespace and wrapping group, and [$name: $shape] objects are used to name the shape elements.

The following are some important shapes:


A substitution represents a piecewise transformation of the kind Atom -> Expr mapped over an expressions atoms. For every var which appears in a given expression, expr replaces every occurence of that atom in the entire expression.

{[var: atom] [expr: expr]}*

NOTE: If two equal var appear in the same substitution, the first one is used.



A rule represents a stateful inference rule which can be joined with substitutions to make a composition.

[top: group] [bot: group]

The top expression is also known as the premise and the bot expression is also known as the conclusion.


A composition represents a chain of rule-substitution pairs composed from top to bottom.

{[rule: {hash | rule}] [substitution: {hash | substitution}]}*


A ruleset is a collection of rules along with a set of substitution constants which are not allowed to be substituted out of. A composition belongs to the closure of a ruleset if all of its rules are in the ruleset and no substitution has any constant as one of its var.

[constants: ( atom* )] [rules: ( {hash | rule}* )]

definition ⚠️

A definition is the assignment of a name and variables to an expression.

def [name: atom] [vars: ( atom* )] [expr: expr]


This shape represents any collection of definitions. For the shape to be a valid set of definitions, it must not contain duplicate name assignments.

{hash | definition}*

Reference Parsers

Currently all expression parsers are built into the reference shell implementations. In the future, they will be separated into their own libraries.


The shell is the default way to interact with QBAR expressions. You can use the shell to build, verify, and analyze compositions and other proof objects.


The following are a list of the currently implemented commands.

NOTE: Commands marked with ⚠️ have an unstable name, API, and/or signature.


clears the screen Same as ^L.

config ⚠️

gets/sets configuration options

docs ⚠️

documentation inside the shell

eval ⚠️

reduces compositions to rules

find ⚠️

looks for expressions

info ⚠️

information about an expression

load ⚠️

loads expressions

ruleset ⚠️

information about a ruleset

search ⚠️

searches for compositions

subst: <expr> <substitution>

substitute out of an expression

tutorial ⚠️

runs the tutorial in the shell

verify ⚠️

verifies that a rule belongs to the composition closure of the given ruleset


prints shell version information


exits the shell Same as exit.


The following are the default shell emacs-like keybindings for the reference shell implementations. Custom and vim-like keybindings are not yet implemented.


line start




exit/restart Same as exit.


line end


clears the screen Same as clear.

Reference Implementations

Worlflow Status Project Crate Documentation

The qbar toolkit comes with two reference shell implementations written in Rust:


The reference terminal shell can be installed with cargo as follows:

cargo install qbar

For more information on the terminal shell implementation see the Rust documentation.


The reference web shell is built off of the reference terminal shell and can be accessed on the main qbar website. For more information on the web shell implementation see the Rust documentation.