Introduced new and extended existing proof rules to allow to remove and add quantifiers, to rewrite in quantified formulas, and to deal with implied formulas instead of equivalent formulas.
Note: Contains also some (less or un-related) changes in the solver for quantified formulas.
Todo: documentation, quantified aux literals, avoid code duplication in Clausifier and SubstitutionHelper
Extended proof system for quantified formulas.
Introduced new and extended existing proof rules to allow to remove and add quantifiers, to rewrite in quantified formulas, and to deal with implied formulas instead of equivalent formulas. Note: Contains also some (less or un-related) changes in the solver for quantified formulas.
Todo: documentation, quantified aux literals, avoid code duplication in Clausifier and SubstitutionHelper