等式理論を法とするDPLL遷移系について

Bibliographic Information

Other Title
  • トウシキ リロン オ ホウ ト スル DPLL センイケイ ニ ツイテ
  • On DPLL Transition Systems Modulo Equational Theories

Search this article

Abstract

SMT solvers are tools for deciding satisfiability of formulas under given theories such as arrays, lists, queues and so on. It is however not easy for users of SMT solvers to specify theories since the theories have to be associated with their decision procedures. In this paper, we formulate the procedure for solving the problem of satisfiability modulo an equational theory (SMET) as a state transition system DPLL(R), and propose its implementation scheme. DPLL(R) generates a decision procedure from a given equational theory and use it to solve the SMET problem. Thus, users can specify equational theories without giving decision procedures.

Journal

References(8)*help

See more

Related Projects

See more

Details 詳細情報について

Report a problem

Back to top