Any theorem proofed and verified by LogicVerifer contributes a wiki page. In the wiki page, the following is included:

1. The name of the theorem
2. Original author
3. Formal statements (In human language)
4. Details explanation of the theorem (In human language)
5. Underlying model
6. Symbolic statements
7. Axiomatic system used
8. Proof section in mathematical statements
   • Link to lemmas, propositions and axioms used
   • Deduction rules applied
   • Note that a page could only be published if every steps here is verified by LV
9. Proof section in human language (or generated by LV)

This seems to be unnecessary. The reason to convert to normal form or canonical normal form is to make equality comparison. For example, given two formula F and G composed of same set of atomic formula, we would like to know if their truth table is exactly the same (maybe up to a permutation of atomic formula).

First, with n atomic formula, we could compose 2^(2^n) different formulas. Therefore, to uniquely represents any formula, we need an O(exp(n)) bit string.

Second, if we just compare the truth table of two formula, it take O(exp(n)) time which is the same as converting to CNF.

Currently, I don't think we have faster than exponential time algorithm for this task. Therefore, let's focus on n <= 10.

1. We would like to convert the representation to "closer-to-human-understanding" level at the page. It is ideal to have the formula already making of ~, &, |, <->, ->, <- etc instead of just ~, &.
2. The representation should be efficient to be parsed and computing its truth value.

Syntax is represented by context-free language parser. Implementing 2 rules (or more) * AtomicFormula = {1-9} {0-9} * Formula = AtomicFormula | ~Formula | (Formula & Formula)

1. Semantic is represented by a table for precedence of operator.
2. Truth table for each operator like ~, &, |, <->, etc...

Human usable rules for derivation. Rules like And-introduction, Modus Ponen, etc. e.g. in the form of {A, B} |- (A & B). In the form of

1. A set of Premises (not restricting in size)
2. Derived formula (only one formula is allow, so that future proof would apply this rule only when absolutely necessary.)

1. Define atomic formula and their assigned truth value.

Symbol	Truth Value	Human translation
A	T	It is raining.
B	T	The floor is wet.
C	F	It is indoor.

2. Define premises, system make sure that the assignment models premises (and therefore, consistent),

The semantic definition states that a theory is consistent if and only if it has a model, i.e. there exists an interpretation under which all formulas in the theory are true

Premise	Truth Value
A	T
~C	T
((A & ~C) -> B)	T

3. Proof steps,

Step	Conclusion	Rules	Premises 1	Premises 2
1	(A & ~C)	And-introduction	A	~C
2	B	Modus Ponen	(A & ~C)	((A & ~C) -> B)

4. Conclusion B.

We share refer to a theorem/axiom/lemma/proposition/premises derived as a consequence. We will first have some predefined premises. Each consists of a unique Id and its translation. For consequence, they have their own Id, translation, formula, type and a proof.

Note that for propositional logic, it is known that if a formula is derived from a set of formula, then it is a consequence (soundness). However, we are not going into the details here.

An axiomatic system include axioms, logic system. User must pick one on the axiomatic system while working on a proof. Example axiomatic system might include PA, ZF, ZFC or some user defined axiomatic system.

Id	Axiomatic System Name	Axioms	Logic System
AS1	User definied AS	{A1, (A1->A2)}	Propositional Logic
AS2	PA	PA axioms	First order logic (?)
AS3	ZFC	ZFC axioms	Second order logic (?)

A proof is a set of statements. A proof can be constructed by smaller/shorter existing proof. Existing proof includes some primitive like And Introduction, De Morgan's laws, Double Negation, which are predefined, and existing proof. Below is an example of proof schema:

Id	Name	Formula
P1	Premise	{A}|-A
P2	Double Negation	{A}|-~~A
P3	And Introduction	{A,B}|-(A&B)
P4	De Morgan's laws 1	{(A&B)}|-~(~A

Id	Translation	Formula	Proof	Axiomatic System
F1	It is raining	A1	Premise (AS1)	AS1
F2	It is raining only if it is cloudy	(A1->A2)	Premise (AS1)	AS1
F3	It is cloudy	A2	Modus Ponens (F1,F2)	AS1
F4	It is raining and it is cloudy	(A1&A2)	And Introduction (F1,F3)	AS1
F5	It is not "not raining or not cloudy"	~(~A1|~A2)	De Morgan's laws (F4), Double Negation (F1, F3)	AS1

Note that we don't need to construct a wiki page for each immediate result, but only the important one.

Our parser should support parsing UTF8 string which composes of the following. Any axioms, propositions, theorems are represented by their id (non-zero trailing ).

1. Not ~A
2. And (A&B)
3. Or (A|B)
4. If and only if (A<->B)
5. If (A<-B)
6. Only if (A->B)