EPICProver 0.1.0

A proof system for modal logic with cluster moderator architecture

EPICLogic — Library for Logical Deduction

Table of Contents

• Main Information
• Module operators
• Class opertree
• Class derivedFormula
• Class inferenceRule
• Class provenTheorem
• Class proofTree
• Functions proven_theorems and isDerived
• Function premise_subs

---

↑ Back to top

Installation

You can install EPICProver using pip:

pip install epicprover

Or, if you want the latest development version directly from GitHub:

pip install git+https://github.com/Fivochnik/Eberle-Protsenko-Intuitionistic-Constructive-Prover

↑ Back to top

Main Information

ProEbLogic provides tools for modal logic with custom operators, axioms, inference rules, and proof verification.

All string inputs (formulas, patterns, substitutions) are automatically parsed into opertree objects — the user never needs to work with trees directly.

Key modules:

• operators — operator definitions (names, syntax, types, signatures)
• opertree — internal representation of formulas
• derivedFormula, inferenceRule, provenTheorem, proofTree, metatree — proof system

---

↑ Back to top

Module operators

Contains all operator configuration dictionaries.

Structure	Description
OperatorNameList	Ordered list of operator names
OperatorSyntax	Symbolic notation
Operator	name → numeric ID mapping
OperatorTypeNameList	Formula type names
OperatorTypeName	type name → numeric code
OperatorArgs	Context-specific operator signatures {type_code: {op_id: (arg_types...)}}
PrefixOperators, InfixOperators, PostFixOperators	Lists of operators of the specified fixity
OperatorFixity	A dictionary storing the id of each operation and its fixity
NullaryOperatorHandler	Parsing functions for nullary operators
OperatorDepth	Temporal depth for fixed-point operators

The module is self-documenting: print(operators.__doc__) generates tables of current operators and their signatures.

---

↑ Back to top

Class opertree

Represents a formula as a tree node.

↑ Back to top

Constructor

opertree(type: int, value: list | object = None)

• If value is None, type is interpreted as a string formula and parsed automatically.
• Otherwise, type is a numeric operator ID, value is a list of children (for operators) or a raw value (for nullary operators).

↑ Back to top

Attributes

Attribute	Type	Description
type	int	Operator ID (from Operator dictionary)
value	list[opertree] | object	Children for operators, value for nullary

↑ Back to top

Methods

Method	Description
isCorrectIn(formulaType)	Checks if node arguments are correct for the given formula type
isCorrectAllIn(formulaType)	Recursively checks the entire tree for type correctness
subs(params)	In‑place replacement: parameters ($name) are replaced by trees from params dict
with_subs(params)	Returns a new opertree with parameters replaced by the given substitutions. The original tree remains unchanged
paramValuesFor(other)	Matches tree against other (which may contain parameters $name), returns dict of substitutions
copy()	Returns a shallow copy (nullary values are shared)
__str__	String representation of the tree using OperatorSyntax and OperatorFixity
__repr__	Returns opertree(str(self))
__eq__, __ne__	Structural equality comparison

↑ Back to top

Parameters

• Parameters are denoted by type == 'param' and value is the parameter name (e.g., 'A').
• paramValuesFor returns a dictionary {param_name: opertree} or None if no match.

↑ Back to top

Example

pattern = opertree("$A & ($A -> $B)") — parsed from string
formula = opertree("p & (p -> q)") — also from string
subs = pattern.paramValuesFor(formula) — returns {'A': p, 'B': q}

---

↑ Back to top

Class derivedFormula

Represents a formula that is derivable under certain conditions.

↑ Back to top

Constructor

derivedFormula(tree: str | opertree, cond: dict[str, Callable | None] = {})

• tree — pattern with optional parameters ($A, $B, ...)
• cond — conditions on parameters:
  • None → parameter must be derivable
  • predicate function → parameter must satisfy it

↑ Back to top

String representation

(($A & $B) ← {$A, $B}) — formula derivable if $A and $B are derivable.

---

↑ Back to top

Class inferenceRule

Defines a rule of inference.

↑ Back to top

Constructor

inferenceRule(premise: list[opertree], conclusion: list[opertree])

• premise — list of formulas representing the premise (meta-AND)
• conclusion — list of formulas representing the conclusion (meta-AND)

Example: Modus Ponens

inferenceRule(
    premise = [opertree('$A'), opertree('$A -> $B')],
    conclusion = [opertree('$B')]
)
print(rule)

↑ Back to top

String representation

[$A, ($A -> $B)] → [$B]

---

↑ Back to top

Class provenTheorem

Represents a theorem proven by applying a rule with a substitution.

↑ Back to top

Constructor

provenTheorem(theorem: derivedFormula, rule: inferenceRule, subs: dict[str, str | opertree])

• theorem — the proven formula (with conditions)
• rule — inference rule used
• subs — substitution mapping parameters to formulas

↑ Back to top

Properties

Property	Description
isCorrect	Whether theorem.tree matches rule.conclusion with subs applied
isDerivedIn(axioms)	Whether the premise is derivable from the given axioms

↑ Back to top

String representation

(($A|$B) ← {$A}) from [$A, ($A->$B)] → [$B] with {A: $A, B: ($A|$B)}

---

↑ Back to top

Class proofTree

Represents a complete proof tree returned by isDerived.

↑ Back to top

Constructor

proofTree(target: opertree | provenTheorem, result: bool, reason: str, subproofs: list[proofTree])

↑ Back to top

Methods

Method	Description
toStr(lasts=None, last=False, lvlType: int = 0)	Returns visual proof tree with branches
toStrFull(lasts=None, last=False)	Returns full visual proof tree with branches
__bool__	Returns result — success or failure
__str__	Returns self.toStr()

↑ Back to top

Output format (short mode)

Goal: (A|B) [✔]  ⊢ (A|B)
├─Theorem: ($A|$B) ← {$A} [✔]  (($A|$B) ∈ {($A|$B)}), ⊢ {$A, ($A->($A|$B))}
│ └─Goal: ($A&($A->($A|$B))) [✔]  ⊢ (($A&$B) ← {$A, $B})
│   ├─Goal: $A [✔]  [hyp]
│   └─Goal: ($A->($A|$B)) [✔]  ⊢ (($A->($A|$B)) ← {})
└─Goal: (A|B) [✔]  ⊢ (($A|$B) ← {$A})
  ├─Goal: A [✔]  ⊢ A
  └─Goal: B [✔]  [free]

↑ Back to top

Symbols

• [✔] — success
• [✘] — failure
• [hyp] — assumption
• [free] — free parameter (no proof required)
• ⊢ — "derivable from"
• ← — "derivable from" (in theorems)
• ∈ — "in set"
• ∉ — "not in set"

---

↑ Back to top

Functions proven_theorems and isDerived

proven_theorems(theorems: list[provenTheorem], axioms: list[derivedFormula]) -> list[provenTheorem]

Filters the list of theorems, returning only those that can be proven from the given axioms (iteratively, respecting dependencies).

isDerived(main: str | opertree, axioms: list[derivedFormula], theorems: list[provenTheorem] = None) -> proofTree

Checks if main is derivable from axioms and true theorems from proven_theorems(theorems, axioms).

Returns a proofTree object representing the complete proof (or failure tree).

---

Function premise_subs

premise_subs(premise: list[opertree], hypothesis: list[opertree]) -> generator[dict[str, opertree]]

Finds all possible substitutions that make the list of premises match a list of hypotheses.

Example:

premise = [opertree('$A'), opertree('$A -> $B')]
hypothesis = [opertree('A'), opertree('B'), opertree('A -> C'), opertree('A -> D'), opertree('B -> D')]

for subs in premise_subs(premise, hypothesis):
    print(subs)

Output:

{'A': A, 'B': C}
{'A': A, 'B': D}
{'A': B, 'B': D}

---