Closed olaure01 closed 3 years ago
The proof of !(?!A&1) ⊢ ?!A obtained by the automated prover contains many times the same sequent. I am not sure this occurs often but it could lead to much simpler proofs by applying a loop-removal operation.
!(?!A&1) ⊢ ?!A
The proof of
!(?!A&1) ⊢ ?!Aobtained by the automated prover contains many times the same sequent. I am not sure this occurs often but it could lead to much simpler proofs by applying a loop-removal operation.