0
votes
2answers
44 views

Why this first-order logic formula is not correct?

I'm studing computer science at university, in specific Artificial Intelligence. We are using Otter as Theorem prover. I'm having some problems formalizing this: "John, Mary and Derek are three ...
7
votes
1answer
190 views

Are coinductive proofs necessary?

I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed ...