|
|
--- |
|
|
license: mit |
|
|
tags: |
|
|
- formal-verification |
|
|
- coq |
|
|
- threshold-logic |
|
|
- neuromorphic |
|
|
- logic |
|
|
--- |
|
|
|
|
|
# tiny-Implies-verified |
|
|
|
|
|
Formally verified implication gate (material conditional). Single threshold neuron computing logical implication with 100% accuracy. |
|
|
|
|
|
## Architecture |
|
|
|
|
|
| Component | Value | |
|
|
|-----------|-------| |
|
|
| Inputs | 2 | |
|
|
| Outputs | 1 | |
|
|
| Neurons | 1 | |
|
|
| Parameters | 3 | |
|
|
| Weights | [-1, 1] | |
|
|
| Bias | 0 | |
|
|
| Activation | Heaviside step | |
|
|
|
|
|
## Key Properties |
|
|
|
|
|
- 100% accuracy (4/4 inputs correct) |
|
|
- Coq-proven correctness |
|
|
- Single threshold neuron |
|
|
- Integer weights |
|
|
- Reflexive: Implies(x,x) = true |
|
|
- Ex falso quodlibet: Implies(false,y) = true |
|
|
|
|
|
## Usage |
|
|
|
|
|
```python |
|
|
import torch |
|
|
from safetensors.torch import load_file |
|
|
|
|
|
weights = load_file('implies.safetensors') |
|
|
|
|
|
def implies_gate(x, y): |
|
|
# Heaviside: weighted_sum + bias >= 0 |
|
|
inputs = torch.tensor([float(x), float(y)]) |
|
|
weighted_sum = (inputs * weights['weight']).sum() + weights['bias'] |
|
|
return int(weighted_sum >= 0) |
|
|
|
|
|
# Test |
|
|
print(implies_gate(0, 0)) # 1 (false implies false) |
|
|
print(implies_gate(0, 1)) # 1 (false implies true) |
|
|
print(implies_gate(1, 0)) # 0 (true does not imply false) |
|
|
print(implies_gate(1, 1)) # 1 (true implies true) |
|
|
``` |
|
|
|
|
|
## Verification |
|
|
|
|
|
**Coq Theorem**: |
|
|
```coq |
|
|
Theorem implies_correct : forall x y, implies_circuit x y = implb x y. |
|
|
``` |
|
|
|
|
|
Proven axiom-free with properties: |
|
|
- Reflexivity (x → x) |
|
|
- Ex falso quodlibet (⊥ → y) |
|
|
- Modus ponens structure |
|
|
|
|
|
Full proof: [coq-circuits/Boolean/Implies.v](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/Boolean/Implies.v) |
|
|
|
|
|
## Circuit Operation |
|
|
|
|
|
Input combination produces weighted sum: |
|
|
- (0,0): 0*(-1) + 0*1 + 0 = 0 >= 0 → 1 |
|
|
- (0,1): 0*(-1) + 1*1 + 0 = 1 >= 0 → 1 |
|
|
- (1,0): 1*(-1) + 0*1 + 0 = -1 < 0 → 0 |
|
|
- (1,1): 1*(-1) + 1*1 + 0 = 0 >= 0 → 1 |
|
|
|
|
|
Fails only when antecedent is true and consequent is false. |
|
|
|
|
|
## Citation |
|
|
|
|
|
```bibtex |
|
|
@software{tiny_implies_prover_2025, |
|
|
title={tiny-Implies-verified: Formally Verified Implication Gate}, |
|
|
author={Norton, Charles}, |
|
|
url={https://huggingface.co/phanerozoic/tiny-Implies-verified}, |
|
|
year={2025} |
|
|
} |
|
|
``` |
|
|
|
