Talk:Satisfiability modulo theories

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Clconway (talk | contribs) at 16:53, 8 October 2008 (→‎Basic terminology: response in re decidability). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Basic terminology

I think the article should be more precise on what formulas can be instances of a SMT. For example, satisfiability of formulas in first order predicate logic is undecidable. The same is true for first-order arithmetic over N. --Borishollas (talk) 16:28, 7 October 2008 (UTC)[reply]

I don't think the decidability of the underlying theories is relevant to whether a formula is or is not an SMT instance. SMT solvers like Simplify and CVC incorporate semidecision procedures for quantified arithmetic formulas. Clconway (talk) 16:53, 8 October 2008 (UTC)[reply]

CVC merge

I think we should probably just delete the CVC article and information rather than copy-and-paste it into this one. It's out of place where it is now. Clconway (talk) 14:15, 6 June 2008 (UTC)[reply]

Retrieved from "https://en.wikipedia.org/w/index.php?title=Talk:Satisfiability_modulo_theories&oldid=243926599"