Tope sequent \( \Xi \mid \Phi \vdash \psi \).

Pretty-print a Sequent.

>>> points = [("t", "I"), ("s", "J")]
>>> topes = [("φ" `TopeOr` "ζ") `TopeAnd` ("ψ" `TopeOr` "χ"), ("t" `TopeEQ` "s")]
>>> putStrLn (ppSequent (Sequent points topes ("s" `TopeEQ` "t")))
t : I, s : J | (φ ∨ ζ) ∧ (ψ ∨ χ), t ≡ s ⊢ s ≡ t

A name of a (tope inference) rule.

A collection of tope inference rules. Intuitively, Rules is a non-deterministic function from Sequent to (RuleName, [Sequent]).

A collection of generalized tope inference rules. Intuitively, RulesM a is a non-deterministic function from Sequent to a.

Rules, collected by type.

Rules for intuitionistic tope logic:

• axiom rule
• \(\land\)-rules (leftAnd and rightAnd)
• \(\lor\)-rules (leftOr, rightOrL, and rightOrR)
• \(\Rightarrow\)-rules (leftImplies, rightImplies)

Rules for tope equality:

• reflexivity (reflEQ)
• symmetry (symEQ)
• transitivity (transEQ)
• substitution (substEQ)

Rules for intuitionistic tope logic with equality:

• intuitionistic rules rulesLJ
• equality tope rules rulesEQ

Rules for inequality tope (not built-in).

• reflexivity (reflLEQ)
• antisymmetry (antisymLEQ)
• transitivity (transLEQ)
• excluded middle (lemLEQ)
• infimum (zeroLEQ)
• supremum (oneLEQ)
• distinctness of 0 and 1 (distinctLEQ)

Transitivity rule for equality tope (see TopeEQ).

———————————
 ⋅ ⊢ x ≡ x

Transitivity rule for equality tope (see TopeEQ).

     x ≡ y, y ≡ z ⊢ φ
—————————————————————————
 x ≡ y, y ≡ z, x ≡ z ⊢ φ

Symmetry rule for equality tope (see TopeEQ).

    x ≡ y ⊢ φ
——————————————————
 x ≡ y, y ≡ x ⊢ φ

Substitution rule for equality tope (see TopeEQ).

   Г, x ≡ y ⊢ φ
—————————————————
 Г[yx] ⊢ φ[yx]

NOTE: limited to replacing a variable, not an arbitrary point subterm.

Try the second computation only if the first one fails (i.e. no backtracking).

The following examples show the difference between orElse and mplus for Logic:

>>> observeAll (pure 1 `orElse` pure 2)
[1]
>>> observeAll (pure 1 `mplus` pure 2)
[1,2]

>>> observeAll $ do { x <- pure 1 `orElse` pure 2; guard (even x); return x }
[]
>>> observeAll $ do { x <- pure 1 `mplus` pure 2; guard (even x); return x }
[2]

Nondeterministically select exactly \(N\) elements from a given list, also returning the remaining part of the list.

Nondeterministically select exactly one element from a given list, also returning the remaining part of the list.

Nondeterministically select exactly one element from a given list.

A complete proof is a proof tree without any unfinished parts.

A proof tree parametrized by the type of leaves (unfinished proofs).

Convert a proof tree into a complete proof if possible.

Pretty print a proof tree (in ASCII form).

Extract proof nodes with corresponding depths.

Pretty-print depth-annotated nodes as a ASCII tree-like structure.

>>> putStr $ ppNodesWithDepth (zip [0,1,2,1,2,3,3,2,3] (map show [0..]))
0
├─ 1
│  └─ 2
└─ 3
   ├─ 4
   │  ├─ 5
   │  └─ 6
   └─ 7
      └─ 8

Pretty-print an ASCII tree-like structure based on depth list.

>>> mapM_ putStrLn $ depthsTree [0,1,2,1,2,3,3,2,3]
└─
   ├─
   │  └─
   └─
      ├─
      │  ├─
      │  └─
      └─
         └─

A simple DFS proof search algorithm for a given set of rules.

A simple k-depth proof search algorithm for a given set of rules.

Search for a proof using simple DFS algorithm (see proveWithDFS).

Search for a proof using a combination of BFS and DFS algorithms (see proveWithBFS).

Search for a proof using BFS and print proof tree (see ppProof).

Search for a proof using a combination of BFS and DFS and print proof tree (see ppProof).

Search for a proof using DFS and print proof tree (see ppProof).

>>> putStrLn (ppSequent ex1)
⋅ | (φ ∨ ζ) ∧ (ψ ∨ χ) ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ

>>> proveAndPrintBFS 8 (fromDefinedRules rulesLJ) ex1
[∧L]  ⋅ | (φ ∨ ζ) ∧ (ψ ∨ χ) ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
└─ [∨L]  ⋅ | φ ∨ ζ, ψ ∨ χ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
   ├─ [∨L]  ⋅ | φ, ψ ∨ χ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
   │  ├─ [∨R₁]  ⋅ | ψ, φ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
   │  │  └─ [∧R]  ⋅ | ψ, φ ⊢ φ ∧ ψ
   │  │     ├─ [Ax]  ⋅ | ψ, φ ⊢ φ
   │  │     └─ [Ax]  ⋅ | ψ, φ ⊢ ψ
   │  └─ [∨R₂]  ⋅ | χ, φ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
   │     └─ [∨R₂]  ⋅ | χ, φ ⊢ ζ ∧ ψ ∨ χ
   │        └─ [Ax]  ⋅ | χ, φ ⊢ χ
   └─ [∨L]  ⋅ | ζ, ψ ∨ χ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
      ├─ [∨R₂]  ⋅ | ψ, ζ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
      │  └─ [∨R₁]  ⋅ | ψ, ζ ⊢ ζ ∧ ψ ∨ χ
      │     └─ [∧R]  ⋅ | ψ, ζ ⊢ ζ ∧ ψ
      │        ├─ [Ax]  ⋅ | ψ, ζ ⊢ ζ
      │        └─ [Ax]  ⋅ | ψ, ζ ⊢ ψ
      └─ [∨R₂]  ⋅ | χ, ζ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
         └─ [∨R₂]  ⋅ | χ, ζ ⊢ ζ ∧ ψ ∨ χ
            └─ [Ax]  ⋅ | χ, ζ ⊢ χ

>>> putStrLn (ppSequent ex2)
⋅ | φ ∧ ψ ∨ ζ ∧ χ ⊢ (φ ∨ ζ) ∧ (ψ ∨ χ)

>>> proveAndPrintBFS 8 (fromDefinedRules rulesLJ) ex2
[∧R]  ⋅ | φ ∧ ψ ∨ ζ ∧ χ ⊢ (φ ∨ ζ) ∧ (ψ ∨ χ)
├─ [∨L]  ⋅ | φ ∧ ψ ∨ ζ ∧ χ ⊢ φ ∨ ζ
│  ├─ [∧L]  ⋅ | φ ∧ ψ ⊢ φ ∨ ζ
│  │  └─ [∨R₁]  ⋅ | φ, ψ ⊢ φ ∨ ζ
│  │     └─ [Ax]  ⋅ | φ, ψ ⊢ φ
│  └─ [∧L]  ⋅ | ζ ∧ χ ⊢ φ ∨ ζ
│     └─ [∨R₂]  ⋅ | ζ, χ ⊢ φ ∨ ζ
│        └─ [Ax]  ⋅ | ζ, χ ⊢ ζ
└─ [∨L]  ⋅ | φ ∧ ψ ∨ ζ ∧ χ ⊢ ψ ∨ χ
   ├─ [∧L]  ⋅ | φ ∧ ψ ⊢ ψ ∨ χ
   │  └─ [∨R₁]  ⋅ | φ, ψ ⊢ ψ ∨ χ
   │     └─ [Ax]  ⋅ | φ, ψ ⊢ ψ
   └─ [∧L]  ⋅ | ζ ∧ χ ⊢ ψ ∨ χ
      └─ [∨R₂]  ⋅ | ζ, χ ⊢ ψ ∨ χ
         └─ [Ax]  ⋅ | ζ, χ ⊢ χ

>>> putStrLn (ppSequent ex3)
⋅ | x ≡ y ∧ y ≡ z ⊢ z ≡ x

>>> proveAndPrintBFS 35 (fromDefinedRules rulesLJE) ex3
[∧L]  ⋅ | x ≡ y ∧ y ≡ z ⊢ z ≡ x
└─ [≡L(trans)]  ⋅ | x ≡ y, y ≡ z ⊢ z ≡ x
   └─ [≡L(sym)]  ⋅ | x ≡ z, x ≡ y, y ≡ z ⊢ z ≡ x
      └─ [Ax]  ⋅ | z ≡ x, x ≡ z, x ≡ y, y ≡ z ⊢ z ≡ x

>>> putStrLn (ppSequent ex4)
⋅ | (t ≡ s ∨ t ≡ u) ∧ s ≡ u ⊢ t ≡ s

>>> proveAndPrintBFS 8 (fromDefinedRules rulesLJE) ex4
[∧L]  ⋅ | (t ≡ s ∨ t ≡ u) ∧ s ≡ u ⊢ t ≡ s
└─ [∨L]  ⋅ | t ≡ s ∨ t ≡ u, s ≡ u ⊢ t ≡ s
   ├─ [Ax]  ⋅ | t ≡ s, s ≡ u ⊢ t ≡ s
   └─ [≡L(sym)]  ⋅ | t ≡ u, s ≡ u ⊢ t ≡ s
      └─ [≡L(trans)]  ⋅ | u ≡ t, t ≡ u, s ≡ u ⊢ t ≡ s
         └─ [≡L(sym)]  ⋅ | s ≡ t, u ≡ t, t ≡ u, s ≡ u ⊢ t ≡ s
            └─ [Ax]  ⋅ | t ≡ s, s ≡ t, u ≡ t, t ≡ u, s ≡ u ⊢ t ≡ s

>>> putStrLn (ppSequent ex5)
⋅ | (≤(t, s) ∨ ≤(s, u)) ∧ ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)

>>> proveAndPrintBFS 5 (fromDefinedRules rulesLJE) ex5
[∧L]  ⋅ | (≤(t, s) ∨ ≤(s, u)) ∧ ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
└─ [∨L]  ⋅ | ≤(t, s) ∨ ≤(s, u), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
   ├─ [∨R₁]  ⋅ | ≤(t, s), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
   │  └─ [∨R₁]  ⋅ | ≤(t, s), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t)
   │     └─ [Ax]  ⋅ | ≤(t, s), ≤(t, u) ⊢ ≤(t, u)
   └─ [∨R₁]  ⋅ | ≤(s, u), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
      └─ [∨R₁]  ⋅ | ≤(s, u), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t)
         └─ [Ax]  ⋅ | ≤(s, u), ≤(t, u) ⊢ ≤(t, u)