Natural_deduction

For handling input from files and stdin, and output to stdout and stderr.

The abstract formula type (and its sub-types).

Parser for mapping formula strings to objects of type FML_types.t_fml.

Lexer for parsing formula strings.

For parsing, printing, and manipulating formulas.

For splitting strings into utf-8 grapheme clusters.

For mapping two-dimensional natural deduction proof trees onto one-dimensional proof sequences of type PRF_sequencer.t_prf_seq.

The abstract proof types (and their sub-types).

Parser for mapping objects of type PRF_sequencer.t_prf_seq to objects of type PRF_types.t_prf_raw.

Lexer for parsing objects of type PRF_sequencer.t_prf_seq.

For parsing, printing, and manipulating proofs.

The abstract type of definitions and proofs (items).

Parser for mapping files containing definitions and proofs to objects of type ITM_types.t_itm list.

Lexer for parsing deinitions and proofs (items).

For expanding formulas and proofs containing defined expressions, replacing each defined expression with its defining expression.

For validating natural deduction proofs in first-order { classical | intuitionistic | minimal } logic.

Comand-line interface for module Main.