Metadata-Version: 2.4
Name: EPICProver
Version: 0.1.0
Summary: A proof system for modal logic with cluster moderator architecture
Author-email: Eberle Vladislav Stanislavovich <eberlad03@gmail.com>, Protsenko Nikita Alexandrovich <nikitaprotsenko2003@gmail.com>
License: MIT
Project-URL: Homepage, https://github.com/Fivochnik/Eberle-Protsenko-Intuitionistic-Constructive-Prover
Project-URL: Bug Tracker, https://github.com/Fivochnik/Eberle-Protsenko-Intuitionistic-Constructive-Prover/issues
Classifier: Programming Language :: Python :: 3
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Requires-Python: >=3.8
Description-Content-Type: text/markdown
License-File: LICENSE
Dynamic: license-file

# EPICLogic — Library for Logical Deduction

## Table of Contents
- [Main Information](#main-information)
- [Module `operators`](#module-operators)
- [Class `opertree`](#class-opertree)
- [Class `derivedFormula`](#class-derivedformula)
- [Class `inferenceRule`](#class-inferencerule)
- [Class `provenTheorem`](#class-proventheorem)
- [Class `proofTree`](#class-prooftree)
- [Functions `proven_theorems` and `isDerived`](#functions-proven_theorems-and-isderived)
- [Function `premise_subs`](#function-premise_subs)

---

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## Installation

You can install EPICProver using pip:

```bash
pip install epicprover
```

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

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

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## 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

---

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## 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.

---

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## Class `opertree`

Represents a formula as a tree node.

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### 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).

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### Attributes

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

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### 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 |

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### 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.

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### 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}`

---

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## Class `derivedFormula`

Represents a formula that is derivable under certain conditions.

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### 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

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### String representation

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

---

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## Class `inferenceRule`

Defines a rule of inference.

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### 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

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

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### String representation

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

---

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## Class `provenTheorem`

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

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### 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

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### Properties

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

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### String representation

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

---

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## Class `proofTree`

Represents a complete proof tree returned by `isDerived`.

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### Constructor

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

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### 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()` |

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### Output format (short mode)

```text
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]
```

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

### Symbols

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

---

##### <div align="right">[↑ Back to top](#table-of-contents)</div>

## 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:

```python
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:

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

---
