# Tag Info

Accepted

### Framework or tools to generate theorem prover/solver/reasoner for new logic

There are many related ways you can mechanise your logic. Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using ...
• 8,328
Accepted

### How could an SMT solver be implemented as simple as possible?

What happens next is that we invoke a SMT solver to try to check whether the formula $$x+y < 20 \quad \land \quad x > 10 \quad \land \quad y > 10$$ is satisfiable. The solver tries to ...
• 160k
Accepted

### What are the differences between symbolic execution and SAT solvers?

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on ...
• 7,088
Accepted

• 160k
1 vote
Accepted

### Objective function and constraint satisfaction over a set of multi-attributes elements

I don't see any problem with modeling this as an integer linear program, for example: ...
• 2,053
1 vote

### Is the optimal order of graph vertices s.t. minimizes edges to later vertices a well-known problem?

Layered graph drawing Layered graph drawing is a graph in which the vertices of a directed graph are drawn in horizontal rows or layers with the edges generally directed downwards. . However, graphs ...
• 305
1 vote