Can you suggest any literature (algorithms etc.) that could help with making a library - for constructing proofs in propositional calculus and other possible useful stuff.
The following is the start, where I define axioms as formulae and inference rules in similar way.
Require Import List. Import ListNotations. Inductive prop := | Var: nat -> prop | Neg: prop -> prop | And: prop -> prop -> prop | Or: prop -> prop -> prop | Impl: prop -> prop -> prop. Coercion Var: nat >-> prop. Notation "¬ A" := (Neg A) (at level 20): prop. Notation "A ∧ B" := (And A B) (at level 21, right associativity): prop. Notation "A ∨ B" := (Or A B) (at level 22, right associativity): prop. Notation "A → B" := (Impl A B) (at level 23, right associativity): prop. Open Scope prop. Definition B := 0. Definition C := 1. Definition D := 2. Definition L1 := B → (C → B). (* ... omitted axioms ... *) Definition inference_rule := prod (list prop) prop. Definition MP: inference_rule := ([B → C ; Var B], Var C).