Talk:Satisfiability modulo theories: Difference between revisions

Content deleted Content added

Inline

Revision as of 16:53, 8 October 2008

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]

@@ Line 3: / Line 3: @@
 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.
 --[[User:Borishollas|Borishollas]] ([[User talk:Borishollas|talk]]) 16:28, 7 October 2008 (UTC)
+: 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. [[User:Clconway|Clconway]] ([[User talk:Clconway|talk]]) 16:53, 8 October 2008 (UTC)
 == CVC merge ==