| Engines that can prove various syntactic classes of logical formulas automatically are important in science and engineering. Satisfiability Modulo Theories (SMT) has emerged as a core research approach in this area. For more precise and reliable application of these engines, it is interesting to investigate proof-producing engines. Such an engine can offer higher reliability in analyzing and checking correctness of industrial designs.;SMT solvers are based on propositional satisfiability algorithms augmented with decision procedures for various theories. There are already impressive propositional SAT solvers. Hence, for SMT research, implementing solvers for specific theories and combining the solvers with a propositional SAT solver are being explored intensively. In this work, we research the proof-producing combination of a SAT solver and a decision procedure for the theory of equality with uninterpreted functions. |
