# Tagged Questions

**3**

votes

**1**answer

268 views

### Formal verification of simple equational proofs (as in Universal Algebra…)?

Is there an software package aimed at verfication of simple equational proofs?
I am hoping to avoid the usual overhead involved with First Order Logic or Higher Order Logic verification systems.
...

**10**

votes

**2**answers

2k views

### Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug? [closed]

Technically, it is possible to prove anything in Coq proof assistant [1] (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis ...