# 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 complete tableau-based theorem prover with industrial-grade performance optimizations.
## 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 four-sign system (T, F, M, N) implemented here follow Ferguson's formal definitions. 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
- ⚡ **Industrial performance**: Optimized tableau with sub-millisecond response
- 🖥️ **CLI and API**: Both command-line and programmatic interfaces
- 📚 **Comprehensive docs**: Full documentation with examples
## Quick Start
### Installation
```bash
pip install wkrq
```
### Command Line Usage
```bash
# Test a simple formula
wkrq "p & q"
# Test with specific sign (T, F, M, N)
wkrq --sign=N "p | ~p"
# Show all models
wkrq --models "p | q"
# Display tableau tree
wkrq --tree "p -> q"
# First-order logic with restricted quantifiers
wkrq "[∃X Student(X)]Human(X)"
wkrq "[∀X Human(X)]Mortal(X)"
```
### Python API
```python
from wkrq import Formula, solve, valid, T, F, 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, N) # Can it be undefined?
print(f"Can be undefined: {result.satisfiable}") # True
```
## Three-Valued Logic Semantics
### Formal Language Definition
The language of wKrQ is defined by the following BNF grammar:
```
⟨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`.
## Documentation
- 📖 [CLI Guide](docs/wKrQ_CLI_GUIDE.md) - Complete command-line reference
- 🔧 [API Reference](docs/wKrQ_API_REFERENCE.md) - Full Python API documentation
- 🏗️ [Architecture](docs/wKrQ_ARCHITECTURE.md) - System design and theory
## 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
```
## Theory
wKrQ uses a tableau proof system with four signs:
- **T**: Must be true (t)
- **F**: Must be false (f)
- **M**: Can be true or false (t or f)
- **N**: Must be undefined (e)
This enables systematic proof search in three-valued logic while maintaining classical reasoning as a special case.
**Note**: Our implementation is validated against Ferguson (2021) and uses classical validity with weak Kleene semantics, meaning classical tautologies remain valid. See `FERGUSON_2021_ANALYSIS.md` for comprehensive validation details.
## Performance
Industrial-grade optimizations include:
- O(1) contradiction detection via hash indexing
- Alpha/beta rule prioritization
- Intelligent branch selection
- Early termination strategies
- Optimized tableau construction
## 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},
url={https://github.com/bradleypallen/wkrq}
}
```
## License
MIT License - see [LICENSE](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)
- [Documentation](https://github.com/bradleypallen/wkrq/tree/main/docs)
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",
"author": null,
"author_email": "\"Bradley P. Allen\" <bradley.p.allen@gmail.com>",
"download_url": "https://files.pythonhosted.org/packages/4b/fc/2b63d57ba5d869c82e8b884d18713638672d3949e0adf71dfcf6a3f0a5e6/wkrq-1.0.7.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 Kleene logic with restricted quantification, featuring a complete tableau-based theorem prover with industrial-grade performance optimizations.\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 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.\n\nThe tableau construction algorithms and four-sign system (T, F, M, N) implemented here follow Ferguson's formal definitions. This is a research implementation created for experimental and educational purposes.\n\n## Research Software Disclaimer\n\n\u26a0\ufe0f **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).\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- \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\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, 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# First-order logic with restricted quantifiers\nwkrq \"[\u2203X Student(X)]Human(X)\"\nwkrq \"[\u2200X Human(X)]Mortal(X)\"\n```\n\n### Python API\n\n```python\nfrom wkrq import Formula, solve, valid, T, F, 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 semantics\ntautology = p | ~p\nprint(f\"Valid in Ferguson's system: {valid(tautology)}\") # True (classical tautologies are valid)\n\n# Three-valued reasoning\nresult = solve(p | ~p, N) # Can it be undefined?\nprint(f\"Can be undefined: {result.satisfiable}\") # True\n```\n\n## Three-Valued Logic Semantics\n\n### Formal Language Definition\n\nThe language of wKrQ is defined by the following BNF grammar:\n\n```\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- **t** (true)\n- **f** (false) \n- **e** (undefined/error)\n\n#### Negation (\u00ac)\n| p | \u00acp |\n|---|-----|\n| t | f |\n| f | t |\n| e | e |\n\n#### Conjunction (\u2227)\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| 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| 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)\nThe formula is true iff there exists a domain element d such that both \u03c6(d) and \u03c8(d) are true. It is false iff for all domain elements d, either \u03c6(d) is false or \u03c8(d) is false (but not undefined). It is undefined if any evaluation results in undefined.\n\n#### Restricted Universal Quantification: [\u2200X \u03c6(X)]\u03c8(X) \nThe formula is true iff for all domain elements d, either \u03c6(d) is false or \u03c8(d) is true. It is false iff there exists a domain element d such that \u03c6(d) is true and \u03c8(d) is false. It is undefined if any evaluation results in undefined.\n\nThe 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 \u2228 e = t`.\n\n## Documentation\n\n- \ud83d\udcd6 [CLI Guide](docs/wKrQ_CLI_GUIDE.md) - Complete command-line reference\n- \ud83d\udd27 [API Reference](docs/wKrQ_API_REFERENCE.md) - Full Python API documentation\n- \ud83c\udfd7\ufe0f [Architecture](docs/wKrQ_ARCHITECTURE.md) - System design and theory\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## Theory\n\nwKrQ uses a tableau proof system with four signs:\n\n- **T**: Must be true (t)\n- **F**: Must be false (f)\n- **M**: Can be true or false (t or f)\n- **N**: Must be undefined (e)\n\nThis enables systematic proof search in three-valued logic while maintaining classical reasoning as a special case.\n\n**Note**: Our implementation is validated against Ferguson (2021) and uses classical validity with weak Kleene semantics, meaning classical tautologies remain valid. See `FERGUSON_2021_ANALYSIS.md` for comprehensive validation details.\n\n## Performance\n\nIndustrial-grade optimizations include:\n\n- O(1) contradiction detection via hash indexing\n- Alpha/beta rule prioritization \n- Intelligent branch selection\n- Early termination strategies\n- Optimized tableau construction\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 Weak Kleene Logic with Restricted Quantification},\n author={Allen, Bradley P.},\n year={2025},\n url={https://github.com/bradleypallen/wkrq}\n}\n```\n\n## License\n\nMIT License - see [LICENSE](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- [Documentation](https://github.com/bradleypallen/wkrq/tree/main/docs)\n",
"bugtrack_url": null,
"license": null,
"summary": "A Python implementation of a semantic tableau calculus for weak Kleene logic with restricted quantification",
"version": "1.0.7",
"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"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "474d0ec6935a3bd09ecac5e057cc0c6a4a2da588d818800fc2dcc443c3dd990f",
"md5": "f9c03cfc0f39d3b1ed48e7ef23d0763c",
"sha256": "cf32ed4b1483b6c6bf8dea3cc5c002379f7a5b10702a996bef4a80ec900f4ac4"
},
"downloads": -1,
"filename": "wkrq-1.0.7-py3-none-any.whl",
"has_sig": false,
"md5_digest": "f9c03cfc0f39d3b1ed48e7ef23d0763c",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.9",
"size": 27592,
"upload_time": "2025-07-29T16:32:17",
"upload_time_iso_8601": "2025-07-29T16:32:17.909962Z",
"url": "https://files.pythonhosted.org/packages/47/4d/0ec6935a3bd09ecac5e057cc0c6a4a2da588d818800fc2dcc443c3dd990f/wkrq-1.0.7-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "4bfc2b63d57ba5d869c82e8b884d18713638672d3949e0adf71dfcf6a3f0a5e6",
"md5": "54dc9cbfc73bb704e2852c74d0c2a7f2",
"sha256": "d8fc70fd43fe01ffd47732a2b9a0a74ba2b058659156f02316feec617af4188f"
},
"downloads": -1,
"filename": "wkrq-1.0.7.tar.gz",
"has_sig": false,
"md5_digest": "54dc9cbfc73bb704e2852c74d0c2a7f2",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.9",
"size": 89238,
"upload_time": "2025-07-29T16:32:19",
"upload_time_iso_8601": "2025-07-29T16:32:19.505851Z",
"url": "https://files.pythonhosted.org/packages/4b/fc/2b63d57ba5d869c82e8b884d18713638672d3949e0adf71dfcf6a3f0a5e6/wkrq-1.0.7.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-07-29 16:32:19",
"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
