Sequent

Sequent is a small proof language and command-line checker for natural deduction proofs in propositional and first-order logic.

The accompanying web application lives outside this repository.

Installation

Download latest release

You can download the prebuilt binaries directly from this repository. All major platforms are accommodated, and SHA256 checksums are provided for checking the integrity of the downloaded binaries.

Build from source

Sequent currently builds with Stack:

stack test
stack build

Install sequent-cli locally:

stack install

Quick Start

Check the showcase program:

sequent-cli check program.seq

Format a source file:

sequent-cli format program.seq

Both commands read from a file, from -, or from stdin when no file is given:

sequent-cli check [FILE|-]
sequent-cli format [FILE|-]

check prints one status line per proof:

identity: AOK
unfinished: Open
broken: Failed

Exit codes:

• 0: every checked proof is AOK and the checker reported no errors.
• 1: parsing failed, or the checker found an error.
• 2: checking succeeded, but at least one proof is open.

format parses the source and writes normalized Sequent source to stdout. The formatter prints the parsed AST, so comments are not preserved.

Language Sketch

A file contains declarations and directives. A proof declaration has a name, a sequent, and a bracketed proof body:

identity : p |- p [
    l1 : p by premise;
    l2 : p by copy l1;
]

Boxes introduce local assumptions:

self_implication : |- p => p [
    @self [
        l1 : p by assumption;
        l2 : p by copy l1;
    ]
    l3 : p => p by imp_i @self;
]

Boxes can also introduce arbitrary variables for first-order rules:

universal_identity : all x. P(x) |- all y. P(y) [
    l1 : all x. P(x) by premise;
    @any [ var y0;
        l2 : P(y0) by all_e l1;
        l3 : P(y0) by copy l2;
    ]
    l4 : all y. P(y) by all_i @any;
]

Formula syntax:

Meaning	Syntax
Negation	~p
Conjunction	p /\ q
Disjunction	p \/ q
Implication	p => q
Falsity	bot
Truth	top
Universal quantifier	all x. P(x)
Existential quantifier	exi x. P(x)
Equality	a = b
Predicate application	P(a, f(b))
Sequent	`p, q

See program.seq and test/Fixtures/ for larger examples.

Repository Layout

• src/: core lexer, parser, AST, formatter, checker, and diagnostics.
• app/sequent-cli/: CLI entry point and rendering.
• test/: regression tests and fixture programs.
• program.seq: small showcase program.