Hugging Face's logo

phanerozoic
/
tiny-Implies-verified

formal-verification
coq
threshold-logic
neuromorphic
logic
Model card Files
xet
Community
tiny-Implies-verified
File size: 2,114 Bytes 
9680d55
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
 
---
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}
}
```