# wKrQ: A Python Implementation of a Semantic Tableau Calculus for Weak Kleene Logic with Restricted Quantification
[](https://badge.fury.io/py/wkrq)
[](https://www.python.org/downloads/)
[](https://opensource.org/licenses/MIT)
[](https://github.com/bradleypallen/wkrq/actions/workflows/tests.yml)
An implementation of a semantic tableau calculus for first-order weak
Kleene logic with restricted quantification, featuring a command-line
interface for satisfiability and inference checking.
## Citation
This implementation is based on the wKrQ tableau system defined in:
**Ferguson, Thomas Macaulay**. "Tableaux and restricted quantification for
systems related to weak Kleene logic." In *International Conference on
Automated Reasoning with Analytic Tableaux and Related Methods*, pp. 3-19.
Cham: Springer International Publishing, 2021.
The tableau construction algorithms and six-sign system (t, f, e, m, n, v)
implemented here follow Ferguson's formal definitions exactly. This is a research
implementation created for experimental and educational purposes.
## Research Software Disclaimer
⚠️ **This is research software.** While extensively tested, this
implementation may contain errors or behave unexpectedly in edge cases. It
is intended for research, education, and experimentation. Use in production
systems is not recommended without thorough validation. Please report any
issues or unexpected behavior through the [issue
tracker](https://github.com/bradleypallen/wkrq/issues).
## Features
- 🎯 **Three-valued semantics**: true (t), false (f), undefined (e)
- 🔤 **Weak Kleene logic**: Operations with undefined propagate undefinedness
- 🔢 **Restricted quantification**: Domain-bounded first-order reasoning
- 📋 **Ferguson's six-sign system**: t, f, e, m, n, v exactly as in the 2021 paper
- 🔄 **ACrQ extension**: Analytic Containment for paraconsistent/paracomplete reasoning
- ⚡ **Industrial performance**: Optimized tableau with sub-millisecond response
- 🖥️ **CLI and API**: Both command-line and programmatic interfaces
- 📚 **Comprehensive docs**: Full documentation with examples
- 🔍 **Construction tracing**: Step-by-step proof visualization showing all rule applications
## Quick Start
### Installation
```bash
pip install wkrq
```
### Command Line Usage
```bash
# Test a simple formula
wkrq "p & q"
# Test with specific sign (t, f, e, m, n)
wkrq --sign=n "p | ~p"
# Show all models
wkrq --models "p | q"
# Display tableau tree
wkrq --tree "p -> q"
# Show construction trace
wkrq --trace "p & ~p"
# First-order logic with restricted quantifiers
# Unicode syntax:
wkrq "[∃X Student(X)]Human(X)"
wkrq "[∀X Human(X)]Mortal(X)"
# ASCII syntax (easier to type):
wkrq "[exists X Student(X)]Human(X)"
wkrq "[forall X Human(X)]Mortal(X)"
# Inference checking (uses |- turnstile syntax)
wkrq "p & q |- p"
wkrq "[forall X Human(X)]Mortal(X), Human(socrates) |- Mortal(socrates)"
# ACrQ paraconsistent reasoning (handles contradictions gracefully)
wkrq --mode=acrq "Human(alice) & ~Human(alice)" # Satisfiable with glut!
# Interactive theory manager with LLM integration for ACrQ
acrq-llm # Start interactive session
acrq-llm --file examples/example_13_maier_et_al.json # Load existing theory
```
### Python API
```python
from wkrq import Formula, solve, valid, t, f, e, m, n
# Create formulas
p, q = Formula.atoms('p', 'q')
formula = p & (q | ~p)
# Test satisfiability
result = solve(formula, t)
print(f"Satisfiable: {result.satisfiable}")
print(f"Models: {result.models}")
# Test validity - Ferguson uses classical validity with weak Kleene
# semantics
tautology = p | ~p
print(f"Valid in Ferguson's system: {valid(tautology)}") # True (classical
# tautologies are valid)
# Three-valued reasoning
result = solve(p | ~p, e) # Can it be undefined?
print(f"Can be undefined: {result.satisfiable}") # True
# ACrQ paraconsistent reasoning
from wkrq import parse_acrq_formula, SyntaxMode
# Handle contradictions gracefully (no explosion)
contradiction = parse_acrq_formula("Human(alice) & ~Human(alice)")
result = solve(contradiction, t)
print(f"Contradiction satisfiable: {result.satisfiable}") # True (glut allowed)
# Different syntax modes for ACrQ
transparent = parse_acrq_formula("~Human(alice)", SyntaxMode.TRANSPARENT) # Standard syntax
bilateral = parse_acrq_formula("Human*(alice)", SyntaxMode.BILATERAL) # Explicit bilateral
# LLM Integration (requires pip install wkrq[llm])
from wkrq import create_openai_evaluator, ACrQTableau
# One line to create LLM evaluator!
evaluator = create_openai_evaluator(model='gpt-4')
# Use with tableau - LLM provides real-world knowledge
tableau = ACrQTableau(
[SignedFormula(t, parse_acrq_formula("Planet(pluto)"))],
llm_evaluator=evaluator
)
result = tableau.construct() # LLM knows Pluto isn't a planet anymore
```
### Theory Manager
The interactive theory manager provides a powerful environment for building and reasoning with logical theories:
```bash
# Start the ACrQ theory manager with LLM support
acrq-llm
# In the interactive session:
theory> assert Socrates is human
theory> assert All humans are mortal
theory> infer
# Infers: Mortal(socrates)
theory> claim firstManOnTheMoon(armstrong) # LLM verifies: TRUE
theory> claim firstManOnTheMoon(scott) # LLM refutes: FALSE
theory> check # Check satisfiability and detect gluts/gaps
theory> save my_theory.json
```
Key features:
- Natural language assertions with automatic translation
- LLM-verified factual claims with the `claim` command
- Paraconsistent reasoning (handles contradictions without explosion)
- Gap and glut detection for information analysis
- Persistent storage in JSON format
- Integration with LLM providers for fact-checking
See the [Theory Manager Tutorial](docs/THEORY_MANAGER_TUTORIAL.md) for detailed usage.
## Syntax and Semantics
### Formal Language Definition
The language of wKrQ is defined by the following BNF grammar:
```bnf
⟨formula⟩ ::= ⟨atom⟩ | ⟨compound⟩ | ⟨quantified⟩
⟨atom⟩ ::= p | q | r | ... | ⟨predicate⟩
⟨predicate⟩ ::= P(⟨term⟩,...,⟨term⟩)
⟨term⟩ ::= ⟨variable⟩ | ⟨constant⟩
⟨variable⟩ ::= X | Y | Z | ...
⟨constant⟩ ::= a | b | c | ...
⟨compound⟩ ::= ¬⟨formula⟩ | (⟨formula⟩ ∧ ⟨formula⟩) |
(⟨formula⟩ ∨ ⟨formula⟩) | (⟨formula⟩ → ⟨formula⟩)
⟨quantified⟩ ::= [∃⟨variable⟩ ⟨formula⟩]⟨formula⟩ |
[∀⟨variable⟩ ⟨formula⟩]⟨formula⟩
```
### Truth Tables
wKrQ implements **weak Kleene** three-valued logic with truth values:
- **t** (true)
- **f** (false)
- **e** (undefined/error)
#### Negation (¬)
| p | ¬p |
|---|-----|
| t | f |
| f | t |
| e | e |
#### Conjunction (∧)
| p \ q | t | f | e |
|-------|---|---|---|
| **t** | t | f | e |
| **f** | f | f | e |
| **e** | e | e | e |
#### Disjunction (∨)
| p \ q | t | f | e |
|-------|---|---|---|
| **t** | t | t | e |
| **f** | t | f | e |
| **e** | e | e | e |
#### Material Implication (→)
| p \ q | t | f | e |
|-------|---|---|---|
| **t** | t | f | e |
| **f** | t | t | e |
| **e** | e | e | e |
### Quantifier Semantics
#### Restricted Existential Quantification: [∃X φ(X)]ψ(X)
The formula is true iff there exists a domain element d such that both
φ(d) and ψ(d) are true. It is false iff for all domain elements d, either
φ(d) is false or ψ(d) is false (but not undefined). It is undefined if any
evaluation results in undefined.
#### Restricted Universal Quantification: [∀X φ(X)]ψ(X)
The formula is true iff for all domain elements d, either φ(d) is false
or ψ(d) is true. It is false iff there exists a domain element d such that
φ(d) is true and ψ(d) is false. It is undefined if any evaluation results
in undefined.
The key principle of weak Kleene logic is that **any operation involving
an undefined value produces an undefined result**. This differs from strong
Kleene logic where, for example, `t ∨ e = t`.
## ACrQ: Analytic Containment with restricted Quantification
ACrQ extends wKrQ with **bilateral predicates** for paraconsistent and paracomplete reasoning:
### Key Features
- **Paraconsistent**: Handle contradictory information without explosion
- **Paracomplete**: Handle incomplete information without classical assumptions
- **Bilateral predicates**: Each predicate R has a dual R* for independent positive/negative tracking
- **Information states**: Distinguishes true, false, gaps (missing info), and gluts (conflicting info)
### Usage Modes
```python
from wkrq import parse_acrq_formula, SyntaxMode
# Transparent mode (default): Standard syntax, automatic translation
formula1 = parse_acrq_formula("Human(alice) & ~Human(alice)") # Handles gluts
# Bilateral mode: Explicit R/R* syntax required
formula2 = parse_acrq_formula("Human(alice) & Human*(alice)", SyntaxMode.BILATERAL)
# Mixed mode: Both syntaxes allowed
formula3 = parse_acrq_formula("Human(alice) & Robot*(bob)", SyntaxMode.MIXED)
```
### Information States
| State | R(a) | R*(a) | Meaning |
|-------|------|-------|---------|
| True | t | f | Positive evidence only |
| False | f | t | Negative evidence only |
| Gap | f | f | No evidence (incomplete) |
| Glut | t | t | Conflicting evidence (paraconsistent) |
## LLM Integration (ACrQ)
The ACrQ system seamlessly integrates with Large Language Models through the [bilateral-truth](https://github.com/bradleypallen/bilateral-truth) package. This integration is specific to ACrQ because it leverages bilateral predicates to handle LLM uncertainty and conflicting information:
```bash
# Install with LLM support
pip install wkrq[llm]
```
```python
from wkrq import create_openai_evaluator, ACrQTableau, parse_acrq_formula, SignedFormula, t
# One line to connect to your LLM
evaluator = create_openai_evaluator(model='gpt-4') # Or use anthropic, google, local
# Combine formal logic with LLM knowledge
formulas = [
SignedFormula(t, parse_acrq_formula("[∀X Orbits(X, sun)]Planet(X)")), # Formal rule
SignedFormula(t, parse_acrq_formula("Orbits(pluto, sun)")), # Fact
]
tableau = ACrQTableau(formulas, llm_evaluator=evaluator)
result = tableau.construct()
# LLM knows modern astronomy: Pluto isn't a planet → contradiction detected
```
The bilateral-truth package handles all the complexity:
- API connections and authentication
- Prompt engineering for factuality assessment
- Response parsing and error handling
- Caching to minimize API calls
Supported providers: OpenAI, Anthropic, Google, local models (Ollama), and more.
## Documentation
### Core Documentation
- 📖 [CLI Guide](https://github.com/bradleypallen/wkrq/blob/main/docs/CLI.md) - Complete command-line reference with examples
- 🔧 [API Reference](https://github.com/bradleypallen/wkrq/blob/main/docs/API.md) - Full Python API documentation with code examples
- 📋 [Examples Guide](https://github.com/bradleypallen/wkrq/blob/main/docs/EXAMPLES.md) - Comprehensive examples with tableau trees
- 🏗️ [Architecture Overview](https://github.com/bradleypallen/wkrq/blob/main/docs/ARCHITECTURE_OVERVIEW.md) - System design and implementation details
### Ferguson Compliance
- 📚 [Ferguson Definitions](https://github.com/bradleypallen/wkrq/blob/main/docs/FERGUSON_DEFINITIONS.md) - Complete reference to Ferguson (2021)
- ✅ [Implementation Verification](https://github.com/bradleypallen/wkrq/blob/main/docs/IMPLEMENTATION_VERIFICATION.md) - Soundness and completeness analysis
- 🔍 [Soundness/Completeness Update](https://github.com/bradleypallen/wkrq/blob/main/docs/SOUNDNESS_COMPLETENESS_UPDATE.md) - Enhanced verification methodology
### ACrQ and LLM Integration
- 🤖 [LLM Rule Formal Specification](https://github.com/bradleypallen/wkrq/blob/main/docs/LLM_RULE_FORMAL_SPECIFICATION.md) - ACrQ-LLM system specification
- ⚖️ [Bilateral Equivalence](https://github.com/bradleypallen/wkrq/blob/main/docs/BILATERAL_EQUIVALENCE_IMPLEMENTATION.md) - Paraconsistent logic implementation
## Examples
### Philosophical Logic: Sorites Paradox
```python
from wkrq import Formula, solve, T, N
# Model vague predicates with three-valued logic
heap_1000 = Formula.atom("Heap1000") # Clearly a heap
heap_999 = Formula.atom("Heap999") # Borderline case
heap_1 = Formula.atom("Heap1") # Clearly not a heap
# Sorites principle
sorites = heap_1000.implies(heap_999)
# The paradox dissolves with undefined values
result = solve(heap_999, N) # Can be undefined
print(f"Borderline case can be undefined: {result.satisfiable}")
```
### First-Order Reasoning
```python
from wkrq import Formula
# Variables and predicates
x = Formula.variable("X")
human = Formula.predicate("Human", [x])
mortal = Formula.predicate("Mortal", [x])
# Restricted quantification
all_humans_mortal = Formula.restricted_forall(x, human, mortal)
print(f"∀-formula: {all_humans_mortal}") # [∀X Human(X)]Mortal(X)
```
## Development
```bash
# Clone repository
git clone https://github.com/bradleypallen/wkrq.git
cd wkrq
# Install in development mode
pip install -e ".[dev]"
# Run tests
pytest
# Format code
black src tests
ruff check src tests
# Type checking
mypy src
```
## Implementation Approach
The wKrQ package implements a semantic tableau calculus for three-valued weak Kleene logic with restricted quantification. The tableau engine (`tableau.py`) uses a six-sign system (t, f, e, m, n, v) following Ferguson (2021), where t and f represent definite truth values, e represents error/undefined, m represents epistemic uncertainty (both true and false are possible), n represents nontrue (false or undefined), and v is a meta-sign used in rule notation. The core algorithm maintains branches as collections of signed formulas, with hash-based indexing by sign and formula for O(1) contradiction detection. The system applies tableau rules in priority order: alpha-rules (non-branching) before beta-rules (branching), with explicit priority values assigned to each rule type. For quantifier instantiation, the engine tracks ground terms per branch and attempts unification with existing constants before generating fresh ones. Universal quantifiers are re-instantiated with new constants as they appear, with the system tracking which constants have been used for each quantified formula to prevent redundant applications. The implementation supports extension to ACrQ through polymorphic branch creation, where bilateral predicates R and R* are processed independently—t:R(a) generates only t:R(a) rather than also concluding f:R*(a), enabling paraconsistent reasoning where contradictory information (t:R(a) ∧ t:R*(a)) remains satisfiable. Model extraction from open branches assigns truth values based on the signs present: t-signed atoms map to true, f-signed to false, e-signed to undefined, with m-signed atoms arbitrarily assigned (true or false) to maintain completeness.
The ACrQ implementation extends wKrQ's tableau calculus to handle bilateral predicates for paraconsistent reasoning. Each predicate R has an associated dual predicate R*, with the system maintaining bidirectional mappings between them. The `ACrQTableau` class overrides the base tableau's branch creation to use `ACrQBranch` instances that track bilateral predicate pairs. During formula processing, negated predicates in transparent syntax mode are automatically converted: ¬R(x) becomes R*(x). The tableau rules for bilateral predicates differ fundamentally from standard predicates: t:R(x) produces only t:R(x) as a conclusion, while t:R*(x) produces only t:R*(x), without generating complementary constraints. Similarly, f:R(x) yields only f:R(x), and f:R*(x) yields only f:R*(x). The m-sign rules branch on individual predicates (m:R(x) branches to t:R(x) or f:R(x)), while n-sign rules generate knowledge gaps (n:R(x) produces f:R(x) and f:R*(x)). This design permits gluts where both R(a) and R*(a) hold true simultaneously—the `_check_contradiction` method in `ACrQBranch` explicitly allows t:R(a) and t:R*(a) to coexist without closing the branch. Model extraction constructs `ACrQModel` instances containing bilateral valuations: for each predicate-argument combination, the model tracks both positive and negative truth values as a `BilateralTruthValue` object. The semantic evaluator (`ACrQEvaluator`) retrieves the appropriate component based on whether the formula references R (positive component) or R* (negative component), maintaining weak Kleene semantics where any operation involving undefined values produces undefined results.
**Note**: Our implementation is validated against Ferguson (2021) and uses
classical validity with weak Kleene semantics, meaning classical tautologies
remain valid. The implementation has been thoroughly tested against literature
examples - see the [validation examples](https://github.com/bradleypallen/wkrq/blob/main/examples/validation.txt) for comprehensive test results.
## Citation
If you use wKrQ in academic work, please cite:
```bibtex
@software{wkrq2025,
title={wKrQ: A Python Implementation of a Semantic Tableau Calculus for
Weak Kleene Logic with Restricted Quantification},
author={Allen, Bradley P.},
year={2025},
version={1.2.0},
url={https://github.com/bradleypallen/wkrq}
}
```
## License
MIT License - see [LICENSE](https://github.com/bradleypallen/wkrq/blob/main/LICENSE) file for details.
## Links
- [PyPI Package](https://pypi.org/project/wkrq/)
- [GitHub Repository](https://github.com/bradleypallen/wkrq)
- [Issue Tracker](https://github.com/bradleypallen/wkrq/issues)
- [CLI Guide](https://github.com/bradleypallen/wkrq/blob/main/docs/CLI.md)
- [API Reference](https://github.com/bradleypallen/wkrq/blob/main/docs/API.md)
- [Examples](https://github.com/bradleypallen/wkrq/blob/main/examples/README.md)
- [Documentation](https://github.com/bradleypallen/wkrq/blob/main/docs/README.md)
Raw data
{
"_id": null,
"home_page": null,
"name": "wkrq",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.9",
"maintainer_email": "\"Bradley P. Allen\" <bradley.p.allen@gmail.com>",
"keywords": "logic, tableau, automated-reasoning, three-valued-logic, weak-kleene, many-valued-logic, philosophical-logic, theorem-proving, paraconsistent-logic, bilateral-predicates, acrq",
"author": null,
"author_email": "\"Bradley P. Allen\" <bradley.p.allen@gmail.com>",
"download_url": "https://files.pythonhosted.org/packages/4d/c7/095735a05f3df57c7099c442dc747125f874bf2ef9040e7521a0053b6252/wkrq-3.3.2.tar.gz",
"platform": null,
"description": "# wKrQ: A Python Implementation of a Semantic Tableau Calculus for Weak Kleene Logic with Restricted Quantification\n\n[](https://badge.fury.io/py/wkrq)\n[](https://www.python.org/downloads/)\n[](https://opensource.org/licenses/MIT)\n[](https://github.com/bradleypallen/wkrq/actions/workflows/tests.yml)\n\nAn implementation of a semantic tableau calculus for first-order weak\nKleene logic with restricted quantification, featuring a command-line\ninterface for satisfiability and inference checking.\n\n## Citation\n\nThis implementation is based on the wKrQ tableau system defined in:\n\n**Ferguson, Thomas Macaulay**. \"Tableaux and restricted quantification for\nsystems related to weak Kleene logic.\" In *International Conference on\nAutomated Reasoning with Analytic Tableaux and Related Methods*, pp. 3-19.\nCham: Springer International Publishing, 2021.\n\nThe tableau construction algorithms and six-sign system (t, f, e, m, n, v)\nimplemented here follow Ferguson's formal definitions exactly. This is a research\nimplementation created for experimental and educational purposes.\n\n## Research Software Disclaimer\n\n\u26a0\ufe0f **This is research software.** While extensively tested, this\nimplementation may contain errors or behave unexpectedly in edge cases. It\nis intended for research, education, and experimentation. Use in production\nsystems is not recommended without thorough validation. Please report any\nissues or unexpected behavior through the [issue\ntracker](https://github.com/bradleypallen/wkrq/issues).\n\n## Features\n\n- \ud83c\udfaf **Three-valued semantics**: true (t), false (f), undefined (e)\n- \ud83d\udd24 **Weak Kleene logic**: Operations with undefined propagate undefinedness\n- \ud83d\udd22 **Restricted quantification**: Domain-bounded first-order reasoning\n- \ud83d\udccb **Ferguson's six-sign system**: t, f, e, m, n, v exactly as in the 2021 paper\n- \ud83d\udd04 **ACrQ extension**: Analytic Containment for paraconsistent/paracomplete reasoning\n- \u26a1 **Industrial performance**: Optimized tableau with sub-millisecond response\n- \ud83d\udda5\ufe0f **CLI and API**: Both command-line and programmatic interfaces\n- \ud83d\udcda **Comprehensive docs**: Full documentation with examples\n- \ud83d\udd0d **Construction tracing**: Step-by-step proof visualization showing all rule applications\n\n## Quick Start\n\n### Installation\n\n```bash\npip install wkrq\n```\n\n### Command Line Usage\n\n```bash\n# Test a simple formula\nwkrq \"p & q\"\n\n# Test with specific sign (t, f, e, m, n)\nwkrq --sign=n \"p | ~p\"\n\n# Show all models\nwkrq --models \"p | q\"\n\n# Display tableau tree\nwkrq --tree \"p -> q\"\n\n# Show construction trace\nwkrq --trace \"p & ~p\"\n\n# First-order logic with restricted quantifiers\n# Unicode syntax:\nwkrq \"[\u2203X Student(X)]Human(X)\"\nwkrq \"[\u2200X Human(X)]Mortal(X)\"\n\n# ASCII syntax (easier to type):\nwkrq \"[exists X Student(X)]Human(X)\"\nwkrq \"[forall X Human(X)]Mortal(X)\"\n\n# Inference checking (uses |- turnstile syntax)\nwkrq \"p & q |- p\"\nwkrq \"[forall X Human(X)]Mortal(X), Human(socrates) |- Mortal(socrates)\"\n\n# ACrQ paraconsistent reasoning (handles contradictions gracefully)\nwkrq --mode=acrq \"Human(alice) & ~Human(alice)\" # Satisfiable with glut!\n\n# Interactive theory manager with LLM integration for ACrQ\nacrq-llm # Start interactive session\nacrq-llm --file examples/example_13_maier_et_al.json # Load existing theory\n```\n\n### Python API\n\n```python\nfrom wkrq import Formula, solve, valid, t, f, e, m, n\n\n# Create formulas\np, q = Formula.atoms('p', 'q')\nformula = p & (q | ~p)\n\n# Test satisfiability\nresult = solve(formula, t)\nprint(f\"Satisfiable: {result.satisfiable}\")\nprint(f\"Models: {result.models}\")\n\n# Test validity - Ferguson uses classical validity with weak Kleene\n# semantics\ntautology = p | ~p\nprint(f\"Valid in Ferguson's system: {valid(tautology)}\") # True (classical\n # tautologies are valid)\n\n# Three-valued reasoning\nresult = solve(p | ~p, e) # Can it be undefined?\nprint(f\"Can be undefined: {result.satisfiable}\") # True\n\n# ACrQ paraconsistent reasoning\nfrom wkrq import parse_acrq_formula, SyntaxMode\n\n# Handle contradictions gracefully (no explosion)\ncontradiction = parse_acrq_formula(\"Human(alice) & ~Human(alice)\")\nresult = solve(contradiction, t)\nprint(f\"Contradiction satisfiable: {result.satisfiable}\") # True (glut allowed)\n\n# Different syntax modes for ACrQ\ntransparent = parse_acrq_formula(\"~Human(alice)\", SyntaxMode.TRANSPARENT) # Standard syntax\nbilateral = parse_acrq_formula(\"Human*(alice)\", SyntaxMode.BILATERAL) # Explicit bilateral\n\n# LLM Integration (requires pip install wkrq[llm])\nfrom wkrq import create_openai_evaluator, ACrQTableau\n\n# One line to create LLM evaluator!\nevaluator = create_openai_evaluator(model='gpt-4')\n\n# Use with tableau - LLM provides real-world knowledge\ntableau = ACrQTableau(\n [SignedFormula(t, parse_acrq_formula(\"Planet(pluto)\"))],\n llm_evaluator=evaluator\n)\nresult = tableau.construct() # LLM knows Pluto isn't a planet anymore\n```\n\n### Theory Manager\n\nThe interactive theory manager provides a powerful environment for building and reasoning with logical theories:\n\n```bash\n# Start the ACrQ theory manager with LLM support\nacrq-llm\n\n# In the interactive session:\ntheory> assert Socrates is human\ntheory> assert All humans are mortal\ntheory> infer\n# Infers: Mortal(socrates)\n\ntheory> claim firstManOnTheMoon(armstrong) # LLM verifies: TRUE\ntheory> claim firstManOnTheMoon(scott) # LLM refutes: FALSE\n\ntheory> check # Check satisfiability and detect gluts/gaps\ntheory> save my_theory.json\n```\n\nKey features:\n- Natural language assertions with automatic translation\n- LLM-verified factual claims with the `claim` command\n- Paraconsistent reasoning (handles contradictions without explosion)\n- Gap and glut detection for information analysis\n- Persistent storage in JSON format\n- Integration with LLM providers for fact-checking\n\nSee the [Theory Manager Tutorial](docs/THEORY_MANAGER_TUTORIAL.md) for detailed usage.\n\n## Syntax and Semantics\n\n### Formal Language Definition\n\nThe language of wKrQ is defined by the following BNF grammar:\n\n```bnf\n\u27e8formula\u27e9 ::= \u27e8atom\u27e9 | \u27e8compound\u27e9 | \u27e8quantified\u27e9\n\n\u27e8atom\u27e9 ::= p | q | r | ... | \u27e8predicate\u27e9\n\n\u27e8predicate\u27e9 ::= P(\u27e8term\u27e9,...,\u27e8term\u27e9)\n\n\u27e8term\u27e9 ::= \u27e8variable\u27e9 | \u27e8constant\u27e9\n\n\u27e8variable\u27e9 ::= X | Y | Z | ...\n\n\u27e8constant\u27e9 ::= a | b | c | ...\n\n\u27e8compound\u27e9 ::= \u00ac\u27e8formula\u27e9 | (\u27e8formula\u27e9 \u2227 \u27e8formula\u27e9) | \n (\u27e8formula\u27e9 \u2228 \u27e8formula\u27e9) | (\u27e8formula\u27e9 \u2192 \u27e8formula\u27e9)\n\n\u27e8quantified\u27e9 ::= [\u2203\u27e8variable\u27e9 \u27e8formula\u27e9]\u27e8formula\u27e9 | \n [\u2200\u27e8variable\u27e9 \u27e8formula\u27e9]\u27e8formula\u27e9\n```\n\n### Truth Tables\n\nwKrQ implements **weak Kleene** three-valued logic with truth values:\n\n- **t** (true)\n- **f** (false) \n- **e** (undefined/error)\n\n#### Negation (\u00ac)\n\n| p | \u00acp |\n|---|-----|\n| t | f |\n| f | t |\n| e | e |\n\n#### Conjunction (\u2227)\n\n| p \\ q | t | f | e |\n|-------|---|---|---|\n| **t** | t | f | e |\n| **f** | f | f | e |\n| **e** | e | e | e |\n\n#### Disjunction (\u2228)\n\n| p \\ q | t | f | e |\n|-------|---|---|---|\n| **t** | t | t | e |\n| **f** | t | f | e |\n| **e** | e | e | e |\n\n#### Material Implication (\u2192)\n\n| p \\ q | t | f | e |\n|-------|---|---|---|\n| **t** | t | f | e |\n| **f** | t | t | e |\n| **e** | e | e | e |\n\n### Quantifier Semantics\n\n#### Restricted Existential Quantification: [\u2203X \u03c6(X)]\u03c8(X)\n\nThe formula is true iff there exists a domain element d such that both\n\u03c6(d) and \u03c8(d) are true. It is false iff for all domain elements d, either\n\u03c6(d) is false or \u03c8(d) is false (but not undefined). It is undefined if any\nevaluation results in undefined.\n\n#### Restricted Universal Quantification: [\u2200X \u03c6(X)]\u03c8(X) \n\nThe formula is true iff for all domain elements d, either \u03c6(d) is false\nor \u03c8(d) is true. It is false iff there exists a domain element d such that\n\u03c6(d) is true and \u03c8(d) is false. It is undefined if any evaluation results\nin undefined.\n\nThe key principle of weak Kleene logic is that **any operation involving\nan undefined value produces an undefined result**. This differs from strong\nKleene logic where, for example, `t \u2228 e = t`.\n\n## ACrQ: Analytic Containment with restricted Quantification\n\nACrQ extends wKrQ with **bilateral predicates** for paraconsistent and paracomplete reasoning:\n\n### Key Features\n\n- **Paraconsistent**: Handle contradictory information without explosion\n- **Paracomplete**: Handle incomplete information without classical assumptions \n- **Bilateral predicates**: Each predicate R has a dual R* for independent positive/negative tracking\n- **Information states**: Distinguishes true, false, gaps (missing info), and gluts (conflicting info)\n\n### Usage Modes\n\n```python\nfrom wkrq import parse_acrq_formula, SyntaxMode\n\n# Transparent mode (default): Standard syntax, automatic translation\nformula1 = parse_acrq_formula(\"Human(alice) & ~Human(alice)\") # Handles gluts\n\n# Bilateral mode: Explicit R/R* syntax required\nformula2 = parse_acrq_formula(\"Human(alice) & Human*(alice)\", SyntaxMode.BILATERAL)\n\n# Mixed mode: Both syntaxes allowed\nformula3 = parse_acrq_formula(\"Human(alice) & Robot*(bob)\", SyntaxMode.MIXED)\n```\n\n### Information States\n\n| State | R(a) | R*(a) | Meaning |\n|-------|------|-------|---------|\n| True | t | f | Positive evidence only |\n| False | f | t | Negative evidence only |\n| Gap | f | f | No evidence (incomplete) |\n| Glut | t | t | Conflicting evidence (paraconsistent) |\n\n## LLM Integration (ACrQ)\n\nThe ACrQ system seamlessly integrates with Large Language Models through the [bilateral-truth](https://github.com/bradleypallen/bilateral-truth) package. This integration is specific to ACrQ because it leverages bilateral predicates to handle LLM uncertainty and conflicting information:\n\n```bash\n# Install with LLM support\npip install wkrq[llm]\n```\n\n```python\nfrom wkrq import create_openai_evaluator, ACrQTableau, parse_acrq_formula, SignedFormula, t\n\n# One line to connect to your LLM\nevaluator = create_openai_evaluator(model='gpt-4') # Or use anthropic, google, local\n\n# Combine formal logic with LLM knowledge\nformulas = [\n SignedFormula(t, parse_acrq_formula(\"[\u2200X Orbits(X, sun)]Planet(X)\")), # Formal rule\n SignedFormula(t, parse_acrq_formula(\"Orbits(pluto, sun)\")), # Fact\n]\n\ntableau = ACrQTableau(formulas, llm_evaluator=evaluator)\nresult = tableau.construct()\n# LLM knows modern astronomy: Pluto isn't a planet \u2192 contradiction detected\n```\n\nThe bilateral-truth package handles all the complexity:\n- API connections and authentication\n- Prompt engineering for factuality assessment\n- Response parsing and error handling\n- Caching to minimize API calls\n\nSupported providers: OpenAI, Anthropic, Google, local models (Ollama), and more.\n\n## Documentation\n\n### Core Documentation\n- \ud83d\udcd6 [CLI Guide](https://github.com/bradleypallen/wkrq/blob/main/docs/CLI.md) - Complete command-line reference with examples\n- \ud83d\udd27 [API Reference](https://github.com/bradleypallen/wkrq/blob/main/docs/API.md) - Full Python API documentation with code examples\n- \ud83d\udccb [Examples Guide](https://github.com/bradleypallen/wkrq/blob/main/docs/EXAMPLES.md) - Comprehensive examples with tableau trees\n- \ud83c\udfd7\ufe0f [Architecture Overview](https://github.com/bradleypallen/wkrq/blob/main/docs/ARCHITECTURE_OVERVIEW.md) - System design and implementation details\n\n### Ferguson Compliance\n- \ud83d\udcda [Ferguson Definitions](https://github.com/bradleypallen/wkrq/blob/main/docs/FERGUSON_DEFINITIONS.md) - Complete reference to Ferguson (2021)\n- \u2705 [Implementation Verification](https://github.com/bradleypallen/wkrq/blob/main/docs/IMPLEMENTATION_VERIFICATION.md) - Soundness and completeness analysis\n- \ud83d\udd0d [Soundness/Completeness Update](https://github.com/bradleypallen/wkrq/blob/main/docs/SOUNDNESS_COMPLETENESS_UPDATE.md) - Enhanced verification methodology\n\n### ACrQ and LLM Integration\n- \ud83e\udd16 [LLM Rule Formal Specification](https://github.com/bradleypallen/wkrq/blob/main/docs/LLM_RULE_FORMAL_SPECIFICATION.md) - ACrQ-LLM system specification\n- \u2696\ufe0f [Bilateral Equivalence](https://github.com/bradleypallen/wkrq/blob/main/docs/BILATERAL_EQUIVALENCE_IMPLEMENTATION.md) - Paraconsistent logic implementation\n\n## Examples\n\n### Philosophical Logic: Sorites Paradox\n\n```python\nfrom wkrq import Formula, solve, T, N\n\n# Model vague predicates with three-valued logic\nheap_1000 = Formula.atom(\"Heap1000\") # Clearly a heap\nheap_999 = Formula.atom(\"Heap999\") # Borderline case\nheap_1 = Formula.atom(\"Heap1\") # Clearly not a heap\n\n# Sorites principle\nsorites = heap_1000.implies(heap_999)\n\n# The paradox dissolves with undefined values\nresult = solve(heap_999, N) # Can be undefined\nprint(f\"Borderline case can be undefined: {result.satisfiable}\")\n```\n\n### First-Order Reasoning\n\n```python\nfrom wkrq import Formula\n\n# Variables and predicates\nx = Formula.variable(\"X\")\nhuman = Formula.predicate(\"Human\", [x])\nmortal = Formula.predicate(\"Mortal\", [x])\n\n# Restricted quantification\nall_humans_mortal = Formula.restricted_forall(x, human, mortal)\nprint(f\"\u2200-formula: {all_humans_mortal}\") # [\u2200X Human(X)]Mortal(X)\n```\n\n## Development\n\n```bash\n# Clone repository\ngit clone https://github.com/bradleypallen/wkrq.git\ncd wkrq\n\n# Install in development mode\npip install -e \".[dev]\"\n\n# Run tests\npytest\n\n# Format code\nblack src tests\nruff check src tests\n\n# Type checking\nmypy src\n```\n\n## Implementation Approach\n\nThe wKrQ package implements a semantic tableau calculus for three-valued weak Kleene logic with restricted quantification. The tableau engine (`tableau.py`) uses a six-sign system (t, f, e, m, n, v) following Ferguson (2021), where t and f represent definite truth values, e represents error/undefined, m represents epistemic uncertainty (both true and false are possible), n represents nontrue (false or undefined), and v is a meta-sign used in rule notation. The core algorithm maintains branches as collections of signed formulas, with hash-based indexing by sign and formula for O(1) contradiction detection. The system applies tableau rules in priority order: alpha-rules (non-branching) before beta-rules (branching), with explicit priority values assigned to each rule type. For quantifier instantiation, the engine tracks ground terms per branch and attempts unification with existing constants before generating fresh ones. Universal quantifiers are re-instantiated with new constants as they appear, with the system tracking which constants have been used for each quantified formula to prevent redundant applications. The implementation supports extension to ACrQ through polymorphic branch creation, where bilateral predicates R and R* are processed independently\u2014t:R(a) generates only t:R(a) rather than also concluding f:R*(a), enabling paraconsistent reasoning where contradictory information (t:R(a) \u2227 t:R*(a)) remains satisfiable. Model extraction from open branches assigns truth values based on the signs present: t-signed atoms map to true, f-signed to false, e-signed to undefined, with m-signed atoms arbitrarily assigned (true or false) to maintain completeness.\n\nThe ACrQ implementation extends wKrQ's tableau calculus to handle bilateral predicates for paraconsistent reasoning. Each predicate R has an associated dual predicate R*, with the system maintaining bidirectional mappings between them. The `ACrQTableau` class overrides the base tableau's branch creation to use `ACrQBranch` instances that track bilateral predicate pairs. During formula processing, negated predicates in transparent syntax mode are automatically converted: \u00acR(x) becomes R*(x). The tableau rules for bilateral predicates differ fundamentally from standard predicates: t:R(x) produces only t:R(x) as a conclusion, while t:R*(x) produces only t:R*(x), without generating complementary constraints. Similarly, f:R(x) yields only f:R(x), and f:R*(x) yields only f:R*(x). The m-sign rules branch on individual predicates (m:R(x) branches to t:R(x) or f:R(x)), while n-sign rules generate knowledge gaps (n:R(x) produces f:R(x) and f:R*(x)). This design permits gluts where both R(a) and R*(a) hold true simultaneously\u2014the `_check_contradiction` method in `ACrQBranch` explicitly allows t:R(a) and t:R*(a) to coexist without closing the branch. Model extraction constructs `ACrQModel` instances containing bilateral valuations: for each predicate-argument combination, the model tracks both positive and negative truth values as a `BilateralTruthValue` object. The semantic evaluator (`ACrQEvaluator`) retrieves the appropriate component based on whether the formula references R (positive component) or R* (negative component), maintaining weak Kleene semantics where any operation involving undefined values produces undefined results.\n\n**Note**: Our implementation is validated against Ferguson (2021) and uses\nclassical validity with weak Kleene semantics, meaning classical tautologies\nremain valid. The implementation has been thoroughly tested against literature\nexamples - see the [validation examples](https://github.com/bradleypallen/wkrq/blob/main/examples/validation.txt) for comprehensive test results.\n\n## Citation\n\nIf you use wKrQ in academic work, please cite:\n\n```bibtex\n@software{wkrq2025,\n title={wKrQ: A Python Implementation of a Semantic Tableau Calculus for\n Weak Kleene Logic with Restricted Quantification},\n author={Allen, Bradley P.},\n year={2025},\n version={1.2.0},\n url={https://github.com/bradleypallen/wkrq}\n}\n```\n\n## License\n\nMIT License - see [LICENSE](https://github.com/bradleypallen/wkrq/blob/main/LICENSE) file for details.\n\n## Links\n\n- [PyPI Package](https://pypi.org/project/wkrq/)\n- [GitHub Repository](https://github.com/bradleypallen/wkrq)\n- [Issue Tracker](https://github.com/bradleypallen/wkrq/issues)\n- [CLI Guide](https://github.com/bradleypallen/wkrq/blob/main/docs/CLI.md)\n- [API Reference](https://github.com/bradleypallen/wkrq/blob/main/docs/API.md)\n- [Examples](https://github.com/bradleypallen/wkrq/blob/main/examples/README.md)\n- [Documentation](https://github.com/bradleypallen/wkrq/blob/main/docs/README.md)\n",
"bugtrack_url": null,
"license": null,
"summary": "A Python implementation of a semantic tableau calculus for weak Kleene logic with restricted quantification",
"version": "3.3.2",
"project_urls": {
"Changelog": "https://github.com/bradleypallen/wkrq/releases",
"Documentation": "https://github.com/bradleypallen/wkrq/tree/main/docs",
"Homepage": "https://github.com/bradleypallen/wkrq",
"Issues": "https://github.com/bradleypallen/wkrq/issues",
"Repository": "https://github.com/bradleypallen/wkrq"
},
"split_keywords": [
"logic",
" tableau",
" automated-reasoning",
" three-valued-logic",
" weak-kleene",
" many-valued-logic",
" philosophical-logic",
" theorem-proving",
" paraconsistent-logic",
" bilateral-predicates",
" acrq"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "873755408e2d7e7713c393b6d03e4cfba32ca00cbc0ee41ae24cedb59b06c0e5",
"md5": "76dc36c49746e0ab3690e19371777009",
"sha256": "e769b04adbd54a4f2072c024f82874e774e34233f5b631dbbee2451eb3d7bb62"
},
"downloads": -1,
"filename": "wkrq-3.3.2-py3-none-any.whl",
"has_sig": false,
"md5_digest": "76dc36c49746e0ab3690e19371777009",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.9",
"size": 75409,
"upload_time": "2025-08-25T18:47:33",
"upload_time_iso_8601": "2025-08-25T18:47:33.001722Z",
"url": "https://files.pythonhosted.org/packages/87/37/55408e2d7e7713c393b6d03e4cfba32ca00cbc0ee41ae24cedb59b06c0e5/wkrq-3.3.2-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "4dc7095735a05f3df57c7099c442dc747125f874bf2ef9040e7521a0053b6252",
"md5": "15ec8b64ee408a19defeceabd3fa38f2",
"sha256": "34c9554ffd8662faf6dc67e5e8290f80fd100901fa879fc84beae28b5acf8509"
},
"downloads": -1,
"filename": "wkrq-3.3.2.tar.gz",
"has_sig": false,
"md5_digest": "15ec8b64ee408a19defeceabd3fa38f2",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.9",
"size": 342675,
"upload_time": "2025-08-25T18:47:33",
"upload_time_iso_8601": "2025-08-25T18:47:33.980450Z",
"url": "https://files.pythonhosted.org/packages/4d/c7/095735a05f3df57c7099c442dc747125f874bf2ef9040e7521a0053b6252/wkrq-3.3.2.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-08-25 18:47:33",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "bradleypallen",
"github_project": "wkrq",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "wkrq"
}
JSON
