Systems
This is an initial list of automated reasoning systems that use combination methods in a substantial way.
The comment in parentheses briefly describes the combination issues or methods considered by each system.
Contributions are welcome.
-
Amphion/Meta-Amphion
(a variant of Constrained Resolution plus the Nelson-Oppen method)
-
CVC
(combination of decision procedures into a validity checker
via a novel version of the Nelson-Oppen method)
-
ESC
(integration of decision procedures into an extended static checker,
combination of procedures via the Nelson-Oppen method)
-
EVES/NEVER
(integration of decision procedures into a verification system,
combination of procedures via the Nelson-Oppen method)
-
Omega
(integration of constraint solvers with proof planning
and computer algebra systems with proof planning)
-
PROTEIN
(theory reasoning based on Model Elimination and
Restart Model Elimination)
-
RDL
(integration of decision procedures and conditional rewriting
by means of Constraint Contextual Rewriting)
-
PVS
(integration of decision procedures into a proof checker,
combination of procedures via the Shostak method)
-
STeP
(integration of decision procedures into an extension of the
Davis-Putnam-Loveland-Logeman satisfiability checker,
combination of procedures via the Shostak method)
-
UniMoK
(combination of decision procedures for unification
via the Baader-Schulz method)
Last updated: Jun 2002.