Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.
14

Validity of higher order formulae is in general not decidable and search spaces are huge, so all you can hope to do is to try to find a proof -- assuming it exists -- by cleverly enumerating the proof space (think sledgehammer, aptly named) but that is rough. Humans can play the oracle, providing the key lemmata to guide proof. Automated provers, on the ...


11

Unification is such a fundamental concept in computer science that perhaps at time we even take it for granted. Any time we have a rule or equation or pattern and want to apply it to some data, unification is used to specialize the rule to the data. Or if we want to combine two general but overlapping rules, unification provides us with the most general ...


10

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 the embedded logic awkward. Shallow embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is only possible when the embedded ...


8

Proof assistants such as Isabelle/HOL work on a syntactical level on a logical calculus. Imagine you have the modus ponens rule (MP) $\qquad \displaystyle P\to Q, P\ \Longrightarrow\ Q$ and the proof goal $\qquad \displaystyle (a \lor b) \to (c \land d), a \lor b \ \overset{!}{\Longrightarrow} c\land d$ We humans see immediately that this follows with ...


7

I would say that the classic distinction of "automated theorem proving" (ATP) vs. "interactive theorem proving" (ITP) needs to be reconsidered. If you take a well-known ITP system like Isabelle/HOL today (Isabelle2013 from February 2013), it integrates quite a lot of add-on tools from the ATP portfolio: On-board generic automated proof tools: old-school ...


6

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 find values for $x,y$ that make this formula true. If it finds such a value, then it knows the assume(false) statement is reachable. (I am guessing you meant to ...


4

Let $\varphi(x)$ be the SMT instance, so the task is to find $x$ such that $\varphi(x)$ is true. One approach is to fix a hash function $h$ that maps a value of $x$ to an element of some small set $S$. Then, you randomly select a value $s \in S$, and ask your SMT solver to find a satisfying assignment for the formula $\varphi(x) \land h(x)=s$. If you want ...


4

I assume the formula is $$(x \ne 0) \land (y|2 = z) \land (1<3).$$ We can handle each clause of the conjunction separately. If $x=(b_3,b_4)$, then $x \ne 0$ translates to $$b_3 \lor b_4.$$ If $y=(b_5,b_6)$ and $z=(b_7,b_8)$, then $y|2$ translates to $(b_5|1,b_6)$, which simplifies to $(1,b_6)$ (if you are doing simplification). Now $(1,b_6) = (b_7,...


3

The Simplex algorithm solves the linear programming problem. Linear programming is the problem of optimizing a linear function with inputs $x_1, x_2, \dots, x_n$ subject to a system of linear equations: $$ 0 \leq x_1, \dots, x_n $$ $$ a_{11} x_1 + \dots + a_{1n} x_n \leq b_1 $$ $$ a_{21} x_2 + \dots + a_{2n} x_n \leq b_2 $$ $$ \dots $$ $$ a_{n1} x_1 + \...


3

You may not need a general SMT solver. In this case, you have a bunch of inequalities conjoined together, which you can solve as a linear program. A simpler alternative to an SMT solver is to implement the theory as an add-on to a logic program. Most decent Prolog implementations, for example, have a CLP(R) or CLP(Q) library which can solve equality and ...


3

Your problem can be mapped to problem of finding minimal set of edges $F$ such that $G\backslash F$ is a DAG (each solution for your problem is a solution for this problem and vice versa). This problem is known as minimum feedback arc set problem and is one of Karp's 21 NP-complete problems


2

I don't think it is important to inference engines. The unification algorithm is however very helpful for type inference. These are two very different kinds of inference. Type inference is important to computer science because types are important in the theory of programming languages, which is a significant part of computer science. Types are also close to ...


2

Yes, absolutely. SMT solvers are actually quite well suited for such problems. Unfortunately, the input language to them (SMTLib) is rather machine-oriented, but there are many "high-level" interfaces to many solvers, Z3 itself providing a Python interface, for instance. For this problem, I'll use the Haskell SBV library, which translates your constraints ...


2

Sure, if the user provides inductive invariants, you can try to check the validity of the verification conditions. However, this remains undecidable, as it requires checking the validity of a formula in first-order logic (with quantifiers and array expressions), and that's undecidable. It might be feasible often enough in practice to be useful, especially ...


2

Szymon Stankiewicz is right -- this problem is basically Feedback Arc Set, which is unfortunately NP-complete. But I have to mention that a very similar graph property, which goes by the slightly alarming name of agony, can actually be computed in just $O(m^2)$ time, where $m$ is the number of edges. The agony of a graph is essentially a weighted form of ...


1

I don't see any gap in your understanding. What you wrote looks correct to me. Perhaps the author meant to use the property $P := c \le n+1 \land n \ge 1$. I think with that modification, $P$ becomes 1-inductive but not 0-inductive. I suspect the author was looking for a simple example of a property that is 1-inductive but not 0-inductive, and missed a ...


1

I would use a SAT solver. Use one boolean variable per edge to encode whether that edge is present or not. Encode the type of a node via a one-hot encoding ($k$ variables per node, where $k$ is the number of possible types). Then each constraint you mention should translate directly into a simple formula on a few of these boolean variables. I like Z3 for ...


1

I don't see any problem with modeling this as an integer linear program, for example: maximize V.x st: 1) s.x < 80 2) 20 <= e.x <= 35 3) FR.x >= 5 4a) Wood.x + 2 - 2W >= 2 4b) Stone.x + 2W >= 2 5) Gold.x - Stone.x < 0 6) Size10p.x <= 5 x[i] ∈ {0, 1} W ∈ {0, 1} Where . is the dot product, x is a binary vector indicating which items ...


1

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 often contain cycles, minimizing the number of inconsistently-oriented edges is NP-hard, and minimizing the number of crossings is also NP-hard. source: ...


1

SMT solvers do support uninterpreted-functions as part of many logics. If there's a counter-example, then they will also print a "counter-example" function, which will be the predicate you're looking for. If you have a concrete example, we can surely see if one can be coded up using Z3.


1

A simple approach would be to simply generate a solution, and then ask for a "different" one, surely? Since you mentioned Haskell, you can use the SBV library to implement this easily, and use the allSat function to generate "different" assignments. Here's an example; not quite the same question as yours but somewhat similar, coded in that style: https://...


Only top voted, non community-wiki answers of a minimum length are eligible