proof-tree-builder.github.io icon indicating copy to clipboard operation
proof-tree-builder.github.io copied to clipboard

Published 20 hours ago • verified publisher icon proof-tree-builder

Symbolic term evaluation

Open joom opened this issue 4 years ago • 0 comments

Currently all term evaluation gets stuck, so we end up with terms like 1 + 1. It's not possible to prove things like P(1 + 1) |- P(2) without the Z3 rule, but it should be.

joom avatar May 29 '20 11:05 joom