# Tag Info

## New answers tagged smt-solvers

0

Your answers to (a) and (c) are correct. To tell whether (b) is correct we need a precise notion of expressiveness. The issue is that propositional logic and first-order logic have totally different semantics: their notions of "model" are valuation and structure respectively. When two logics use the same notion of "model" we can ...

1

If the constraints you have are of the form $a < b$ and $a=b$ (i.e., only unconditional inequality constraints), you can model them with a directed graph: each node represents a variable, and an edge $v \to w$ corresponds to the inequality $v < w$. Then you can answer queries by doing a straightforward reachability check. (If you see the equality $v=... 0 Is there a specific language you must write that in? If not, then if all you need are questions of type$x = y$? and$x < y$?, I would say Prolog is a safe bet. You could just load your equalities and inequalities as rules and then add a general rule that says that$<$and$=$relations are transitive and$=\$ is also reflexive and then you could ask a ...

Top 50 recent answers are included