diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-12-08 00:54:11 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-07 21:54:11 -0600 |
| commit | 57241d382490eed0c480f234dc8cf1c18c1fa525 (patch) | |
| tree | 964f62677f0870ef327fa758622c114ad9d6a93c /test/regress/regress0 | |
| parent | ca4f71c3c3c0da881e0bb9b93dbbb2bb3fe49c46 (diff) | |
[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)
Previously CHAIN_RESOLUTION's definition and checker were not properly capturing its intended behavior as merely an n-ary RESOLUTION rule (i.e., no factoring nor reordering). A new rule, MACRO_RESOLUTION, now captures this behavior: it combines CHAIN_RESOLUTION, FACTORING, and REORDERING.
This commit also adds a proof checker for the new rule and updates the proof checker of CHAIN_RESOLUTION.
Diffstat (limited to 'test/regress/regress0')
0 files changed, 0 insertions, 0 deletions