Skip to main content

Explore our questions

0 votes
0 answers
4 views

ACL2: Is there a way to check that a Skolem does what it says on the tin?

1 vote
1 answer
38 views

Checking if a goal is *definitely wrong* by testing it against random examples in Coq

1 vote
1 answer
20 views

Applying an axiom from a class in a proof

1 vote
1 answer
66 views

Trying to use 'Equations'

1 vote
1 answer
44 views

ACL2 compile single book on command line

0 votes
0 answers
14 views

ACL2 Prove that the product of two positive numbers is positive

0 votes
2 answers
53 views

Coq can you enter a tactic context inside of a `Fixpoint` definition?

1 vote
2 answers
54 views

Dependent equality in Coq

0 votes
2 answers
51 views

Proving `succ_mul` without using `nth_rewrite`

1 vote
1 answer
34 views

Showing that elements match after reducing list (Lean 4)

2 votes
1 answer
73 views

About the use of command Canonical in Coq for mantaining Record Type information

1 vote
1 answer
59 views

Lean4: Prove that ∑ ii : Fin nn, k (Fin.castLE _ ↑↑ii) = ∑ x : Fin nn, k (Fin.castLE _ ↑↑x) (sums over Fin n)

1 vote
1 answer
118 views

How to implement separate compilation?

3 votes
2 answers
161 views

Enumerating all formulae of any first-order language

Browse more Questions