natural deduction checker

ndc.mod

module ndc.

kind parity type -> type -> type.
type pair (A -> B -> parity A B).

kind term type.
type fapp (string -> list term -> term).

kind formula type.
type atom (string -> list term -> formula).
type contradiction (formula).
type negation (formula -> formula).
type conjunction (formula -> formula -> formula).
type disjunction (formula -> formula -> formula).
type implication (formula -> formula -> formula).
type biconditional (formula -> formula -> formula).
type universal ((term -> formula) -> formula).
type existential ((term -> formula) -> formula).
type equation (term -> term -> formula).
type papp (property -> list term -> formula).

kind property type.
type primitive_property (formula -> property).
type prime_property ((term -> property) -> property).

kind scheme type.
type primitive_scheme (formula -> scheme).
type prime_scheme ((property -> scheme) -> scheme).

kind proof type.
type by_axiom (string -> formula -> proof).
type by_assumption (formula -> proof).
type bottom_intro (formula -> proof -> proof -> proof).
type bottom_elim (formula -> proof -> proof).
type not_intro (formula -> (formula -> proof) -> proof).
type not_elim (formula -> (formula -> proof) -> proof).
type and_intro (formula -> proof -> proof -> proof).
type and_elim1 (formula -> proof -> proof).
type and_elim2 (formula -> proof -> proof).
type or_intro1 (formula -> proof -> proof).
type or_intro2 (formula -> proof -> proof).
type or_elim (formula -> proof -> (formula -> proof) -> (formula -> proof) -> proof).
type ifthen_intro (formula -> (formula -> proof) -> proof).
type ifthen_elim (formula -> proof -> proof -> proof).
type iff_intro (formula -> (formula -> proof) -> (formula -> proof) -> proof).
type iff_elim1 (formula -> proof -> proof -> proof).
type iff_elim2 (formula -> proof -> proof -> proof).
type forall_intro (formula -> (term -> proof) -> proof).
type forall_elim (formula -> proof -> proof).
type exists_intro (formula -> proof -> proof).
type exists_elim (formula -> proof -> (term -> formula -> proof) -> proof).
type eqn_intro (formula -> proof).
type eqn_elim1 (formula -> proof -> proof -> proof).
type eqn_elim2 (formula -> proof -> proof -> proof).

kind meta_proof type.
type mono_proof (proof -> meta_proof).
type poly_proof ((property -> meta_proof) -> meta_proof).

type assoc (A -> B -> list (parity A B) -> o).
assoc A B (pair A B :: _) :- true.
assoc A B (_ :: Pairs) :- assoc A B Pairs.

type copy_term (term -> term -> o).
copy_term (fapp Func Terms1) (fapp Func Terms2) :- copy_terms Terms1 Terms2.

type copy_terms (list term -> list term -> o).
copy_terms nil nil :- true.
copy_terms (Term1 :: Terms1) (Term2 :: Terms2) :- copy_term Term1 Term2, copy_terms Terms1 Terms2.

type copy_formula (formula -> formula -> o).
copy_formula (atom Pred Terms1) (atom Pred Terms2) :- copy_terms Terms1 Terms2.
copy_formula (contradiction) (contradiction) :- true.
copy_formula (negation Formula1) (negation Formula2) :- copy_formula Formula1 Formula2.
copy_formula (conjunction Formula1 Formula2) (conjunction Formula3 Formula4) :- copy_formula Formula1 Formula3, copy_formula Formula2 Formula4. 
copy_formula (disjunction Formula1 Formula2) (disjunction Formula3 Formula4) :- copy_formula Formula1 Formula3, copy_formula Formula2 Formula4.
copy_formula (implication Formula1 Formula2) (implication Formula3 Formula4) :- copy_formula Formula1 Formula3, copy_formula Formula2 Formula4.
copy_formula (biconditional Formula1 Formula2) (biconditional Formula3 Formula4) :- copy_formula Formula1 Formula3, copy_formula Formula2 Formula4. 
copy_formula (universal AbsFormula1) (universal AbsFormula2) :- pi ivar\ copy_term ivar ivar => copy_formula (AbsFormula1 ivar) (AbsFormula2 ivar).
copy_formula (existential AbsFormula1) (existential AbsFormula2) :- pi ivar\ copy_term ivar ivar => copy_formula (AbsFormula1 ivar) (AbsFormula2 ivar).
copy_formula (equation Term1 Term2) (equation Term3 Term4) :- copy_term Term1 Term3, copy_term Term2 Term4.
copy_formula (papp Property1 Terms1) (papp Property2 Terms2) :- copy_property Property1 Property2, copy_terms Terms1 Terms2.

type subst_formula ((term -> formula) -> term -> formula -> o).
subst_formula AbsFormula Term Formula :- pi ivar\ copy_term ivar Term => copy_formula (AbsFormula ivar) Formula.

type copy_property (property -> property -> o).
copy_property (primitive_property PrimitiveProperty1) (primitive_property PrimitiveProperty2) :- copy_formula PrimitiveProperty1 PrimitiveProperty2.
copy_property (prime_property PrimeProperty1) (prime_property PrimeProperty2) :- pi ivar\ copy_term ivar ivar => copy_property (PrimeProperty1 ivar) (PrimeProperty2 ivar).

type match_property_with_args (property -> list term -> formula -> o).
match_property_with_args (primitive_property PrimitiveProperty) nil Formula :- copy_formula PrimitiveProperty Formula.
match_property_with_args (prime_property PrimeProperty) (Term :: Terms) Formula :- sigma Property\ match_property_with_args Property Terms Formula, pi ivar\ copy_term ivar ivar => copy_property (PrimeProperty ivar) Property.

type instantiate_property ((property -> formula) -> formula -> property -> o).
instantiate_property (property\ (atom Pred Terms1)) (atom Pred Terms2) Property :- copy_terms Terms1 Terms2.
instantiate_property (property\ (contradiction)) (contradiction) Property :- true.
instantiate_property (property\ (negation (PrimeFormula1 property))) (negation Formula1) Property :- instantiate_property PrimeFormula1 Formula1 Property.
instantiate_property (property\ (conjunction (PrimeFormula1 property) (PrimeFormula2 property))) (conjunction Formula1 Formula2) Property :- instantiate_property PrimeFormula1 Formula1 Property, instantiate_property PrimeFormula2 Formula2 Property.
instantiate_property (property\ (disjunction (PrimeFormula1 property) (PrimeFormula2 property))) (disjunction Formula1 Formula2) Property :- instantiate_property PrimeFormula1 Formula1 Property, instantiate_property PrimeFormula2 Formula2 Property.
instantiate_property (property\ (implication (PrimeFormula1 property) (PrimeFormula2 property))) (implication Formula1 Formula2) Property :- instantiate_property PrimeFormula1 Formula1 Property, instantiate_property PrimeFormula2 Formula2 Property.
instantiate_property (property\ (universal (ivar\ AbsPrimeFormula1 ivar property))) (universal AbsFormula1) Property :- pi ivar\ copy_term ivar ivar => instantiate_property (AbsPrimeFormula1 ivar) (AbsFormula1 ivar) Property.
instantiate_property (property\ (existential (ivar\ AbsPrimeFormula1 ivar property))) (existential AbsFormula1) Property :- pi ivar\ copy_term ivar ivar => instantiate_property (AbsPrimeFormula1 ivar) (AbsFormula1 ivar) Property.
instantiate_property (property\ (equation Term1 Term2)) (equation Term3 Term4) Property :- copy_term Term1 Term3, copy_term Term2 Term4.
instantiate_property (property\ (papp property Terms)) Formula Property :- match_property_with_args Property Terms Formula.

type test_to_instantiate_property (property -> o).
test_to_instantiate_property Property :- instantiate_property (property\ implication (papp property [fapp "zero" []]) (implication (universal (n\ implication (papp property [n]) (papp property [fapp "succ" [n]]))) (universal (n\ papp property [n])))) (implication (equation (fapp "plus" [fapp "zero" [], fapp "zero" []]) (fapp "zero" [])) (implication (universal (n\ implication (equation (fapp "plus" [n, fapp "zero" []]) n) (equation (fapp "plus" [fapp "succ" [n], fapp "zero" []]) (fapp "succ" [n])))) (universal (n\ equation (fapp "plus" [n, fapp "zero" []]) n)))) Property.

type instantiate_scheme (scheme -> formula -> list property -> o).
instantiate_scheme (primitive_scheme PrimitiveScheme) Formula nil :- copy_formula PrimitiveScheme Formula.
instantiate_scheme (prime_scheme PrimeScheme) Formula (Property :: Properties) :- sigma PrimeFormula\ (pi property\ copy_property property property => instantiate_scheme (PrimeScheme property) (PrimeFormula property) Properties), instantiate_property PrimeFormula Formula Property.

type test_to_instantiate_scheme (list property -> o).
test_to_instantiate_scheme Properties :- instantiate_scheme (prime_scheme (property\ primitive_scheme (implication (papp property [fapp "zero" []]) (implication (universal (n\ implication (papp property [n]) (papp property [fapp "succ" [n]]))) (universal (n\ papp property [n])))))) (implication (equation (fapp "plus" [fapp "zero" [], fapp "zero" []]) (fapp "zero" [])) (implication (universal (n\ implication (equation (fapp "plus" [n, fapp "zero" []]) n) (equation (fapp "plus" [fapp "succ" [n], fapp "zero" []]) (fapp "succ" [n])))) (universal (n\ equation (fapp "plus" [n, fapp "zero" []]) n)))) Properties.

type check_proof (list (parity string scheme) -> proof -> formula -> o).
check_proof Axioms (by_axiom AxiomName Goal) Goal :- sigma Axiom\ assoc AxiomName Axiom Axioms, sigma Properties\ instantiate_scheme Axiom Goal Properties.
check_proof Axioms (by_assumption Goal) Goal :- true.
check_proof Axioms (bottom_intro (contradiction) PrfOfA PrfOfNotA) Goal :- copy_formula contradiction Goal, sigma A\ check_proof Axioms PrfOfA A, check_proof Axioms PrfOfNotA (negation A).
check_proof Axioms (bottom_elim A PrfOfBottom) Goal :- copy_formula A Goal, check_proof Axioms PrfOfBottom contradiction.
check_proof Axioms (not_intro (negation A) PrfOfBottomAssumingA) Goal :- copy_formula (negation A) Goal, check_proof Axioms (PrfOfBottomAssumingA A) contradiction.
check_proof Axioms (not_elim A PrfOfBottomAssumingNotA) Goal :- copy_formula A Goal, check_proof Axioms (PrfOfBottomAssumingNotA (negation A)) contradiction.
check_proof Axioms (and_intro (conjunction A B) PrfOfA PrfOfB) Goal :- copy_formula (conjunction A B) Goal, check_proof Axioms PrfOfA A, check_proof Axioms PrfOfB B.
check_proof Axioms (and_elim1 A PrfOfAAndB) Goal :- copy_formula A Goal, sigma B\ check_proof Axioms PrfOfAAndB (conjunction A B).
check_proof Axioms (and_elim2 B PrfOfAAndB) Goal :- copy_formula B Goal, sigma A\ check_proof Axioms PrfOfAAndB (conjunction A B).
check_proof Axioms (or_intro1 (disjunction A B) PrfOfA) Goal :- copy_formula (disjunction A B) Goal, check_proof Axioms PrfOfA A.
check_proof Axioms (or_intro2 (disjunction A B) PrfOfB) Goal :- copy_formula (disjunction A B) Goal, check_proof Axioms PrfOfB B.
check_proof Axioms (or_elim C PrfOfAOrB PrfOfCAssumingA PrfOfCAssumingB) Goal :- copy_formula C Goal, sigma A\ sigma B\ check_proof Axioms PrfOfAOrB (disjunction A B), check_proof Axioms (PrfOfCAssumingA A) C, check_proof Axioms (PrfOfCAssumingB B) C.
check_proof Axioms (ifthen_intro (implication A B) PrfOfBAssumingA) Goal :- copy_formula (implication A B) Goal, check_proof Axioms (PrfOfBAssumingA A) B.
check_proof Axioms (ifthen_elim B PrfOfIfAThenB PrfOfA) Goal :- copy_formula B Goal, sigma A\ check_proof Axioms PrfOfIfAThenB (implication A B), check_proof Axioms PrfOfA A.
check_proof Axioms (iff_intro (biconditional A B) PrfOfBAssumingA PrfOfAAssumingB) Goal :- copy_formula (biconditional A B) Goal, check_proof Axioms (PrfOfBAssumingA A) B, check_proof Axioms (PrfOfAAssumingB B) A.
check_proof Axioms (iff_elim1 B PrfOfAIffB PrfOfA) Goal :- copy_formula B Goal, sigma A\ check_proof Axioms PrfOfAIffB (biconditional A B), check_proof Axioms PrfOfA A.
check_proof Axioms (iff_elim2 A PrfOfAIffB PrfOfB) Goal :- copy_formula A Goal, sigma B\ check_proof Axioms PrfOfAIffB (biconditional A B), check_proof Axioms PrfOfB B.
check_proof Axioms (forall_intro (universal Alpha) PrfOfAlphaWithVar) Goal :- copy_formula (universal Alpha) Goal, pi ivar\ copy_term ivar ivar => check_proof Axioms (PrfOfAlphaWithVar ivar) (Alpha ivar).
check_proof Axioms (forall_elim A PrfOfForallAlpha) Goal :- copy_formula A Goal, sigma Alpha\ check_proof Axioms PrfOfForallAlpha (universal Alpha), sigma Term\ subst_formula Alpha Term A.
check_proof Axioms (exists_intro (existential Alpha) PrfOfA) Goal :- copy_formula (existential Alpha) Goal, sigma A\ check_proof Axioms PrfOfA A, sigma Term\ subst_formula Alpha Term A.
check_proof Axioms (exists_elim B PrfOfExistsAlpha PrfOfBAssumingAWithVar) Goal :- copy_formula B Goal, sigma Alpha\ check_proof Axioms PrfOfExistsAlpha (existential Alpha), pi ivar\ copy_term ivar ivar => check_proof Axiom (PrfOfBAssumingAWithVar ivar (Alpha ivar)) B.
check_proof Axioms (eqn_intro (equation Term1 Term2)) Goal :- copy_formula (equation Term1 Term2) Goal, copy_term Term1 Term2.
check_proof Axioms (eqn_elim1 AlphaTerm2 PrfOfTerm1EqTerm2 PrfOfAlphaTerm1) Goal :- copy_formula AlphaTerm2 Goal, sigma Term1\ sigma Term2\ check_proof Axioms PrfOfTerm1EqTerm2 (equation Term1 Term2), sigma Alpha\ subst_formula Alpha Term2 AlphaTerm2, check_proof Axioms PrfOfAlphaTerm1 (Alpha Term1).
check_proof Axioms (eqn_elim2 AlphaTerm1 PrfOfTerm1EqTerm2 PrfOfAlphaTerm2) Goal :- copy_formula AlphaTerm1 Goal, sigma Term1\ sigma Term2\ check_proof Axioms PrfOfTerm1EqTerm2 (equation Term1 Term2), sigma Alpha\ subst_formula Alpha Term1 AlphaTerm1, check_proof Axioms PrfOfAlphaTerm2 (Alpha Term2).

type check_meta_proof (list (parity string scheme) -> meta_proof -> scheme -> o).
check_meta_proof Axioms (mono_proof MonoProof) (primitive_scheme PrimitiveScheme) :- check_proof Axioms MonoProof PrimitiveScheme.
check_meta_proof Axioms (poly_proof PolyProof) (prime_scheme PrimeScheme) :- pi property\ copy_property property property => check_meta_proof Axioms (PolyProof property) (PrimeScheme property).

type example1 (o).
example1 :- check_meta_proof [] (poly_proof (p\ mono_proof (not_elim (disjunction (papp p []) (negation (papp p []))) (Hyp1\ bottom_intro contradiction (or_intro2 (disjunction (papp p []) (negation (papp p []))) (not_intro (negation (papp p [])) (Hyp2\ bottom_intro contradiction (or_intro1 (disjunction (papp p []) (negation (papp p []))) (by_assumption Hyp2)) (by_assumption Hyp1)))) (by_assumption Hyp1))))) (prime_scheme (p\ primitive_scheme (disjunction (papp p []) (negation (papp p []))))).

end

ndc.sig

sig ndc.

kind parity type -> type -> type.
kind term type.
kind formula type.
kind property type.
kind scheme type.
kind proof type.
kind meta_proof type.

type pair (A -> B -> parity A B).

type fapp (string -> list term -> term).

type atom (string -> list term -> formula).
type contradiction (formula).
type negation (formula -> formula).
type conjunction (formula -> formula -> formula).
type disjunction (formula -> formula -> formula).
type implication (formula -> formula -> formula).
type biconditional (formula -> formula -> formula).
type universal ((term -> formula) -> formula).
type existential ((term -> formula) -> formula).
type equation (term -> term -> formula).
type papp (property -> list term -> formula).

type primitive_property (formula -> property).
type prime_property ((term -> property) -> property).

type primitive_scheme (formula -> scheme).
type prime_scheme ((property -> scheme) -> scheme).

type by_axiom (string -> formula -> proof).
type by_assumption (formula -> proof).
type bottom_intro (formula -> proof -> proof -> proof).
type bottom_elim (formula -> proof -> proof).
type not_intro (formula -> (formula -> proof) -> proof).
type not_elim (formula -> (formula -> proof) -> proof).
type and_intro (formula -> proof -> proof -> proof).
type and_elim1 (formula -> proof -> proof).
type and_elim2 (formula -> proof -> proof).
type or_intro1 (formula -> proof -> proof).
type or_intro2 (formula -> proof -> proof).
type or_elim (formula -> proof -> (formula -> proof) -> (formula -> proof) -> proof).
type ifthen_intro (formula -> (formula -> proof) -> proof).
type ifthen_elim (formula -> proof -> proof -> proof).
type iff_intro (formula -> (formula -> proof) -> (formula -> proof) -> proof).
type iff_elim1 (formula -> proof -> proof -> proof).
type iff_elim2 (formula -> proof -> proof -> proof).
type forall_intro (formula -> (term -> proof) -> proof).
type forall_elim (formula -> proof -> proof).
type exists_intro (formula -> proof -> proof).
type exists_elim (formula -> proof -> (term -> formula -> proof) -> proof).
type eqn_intro (formula -> proof).
type eqn_elim1 (formula -> proof -> proof -> proof).
type eqn_elim2 (formula -> proof -> proof -> proof).

type mono_proof (proof -> meta_proof).
type poly_proof ((property -> meta_proof) -> meta_proof).

type assoc (A -> B -> list (parity A B) -> o).
type copy_term (term -> term -> o).
type copy_terms (list term -> list term -> o).
type copy_formula (formula -> formula -> o).
type subst_formula ((term -> formula) -> term -> formula -> o).
type copy_property (property -> property -> o).
type match_property_with_args (property -> list term -> formula -> o).
type instantiate_property ((property -> formula) -> formula -> property -> o).
type test_to_instantiate_property (property -> o).
type instantiate_scheme (scheme -> formula -> list property -> o).
type test_to_instantiate_scheme (list property -> o).
type check_proof (list (parity string scheme) -> proof -> formula -> o).
type check_meta_proof (list (parity string scheme) -> meta_proof -> scheme -> o).
type example1 (o).

end