作者： Thomas Sturm , Andreas Seidl
DOI:
关键词:
摘要: We establish a framework to integrate propositional logic with first-order logic. This is done in such way that it optionally appears either as over Boolean algebra or including quantification. describe and prove complexity bounds for extended quantifier elimination by virtual substitution our theory. is, besides many other mathematical algorithms utilities, implemented new context ibalp of the reduce package redlog. demonstrate capabilities this means numerous application benchmark examples qsat problems.