Loge: a guided tour

root = Path.expand("..", __DIR__)

Mix.install([
  {:loge, path: Path.join(root, "loge"), override: true},
  {:loge_tptp, path: Path.join(root, "loge_tptp")},
  {:loge_dimacs, path: Path.join(root, "loge_dimacs")},
  {:loge_asp, path: Path.join(root, "loge_asp")},
  {:loge_prolog, path: Path.join(root, "loge_prolog")},
  {:loge_egglog, path: Path.join(root, "loge_egglog")},
  {:loge_smtlib, path: Path.join(root, "loge_smtlib")},
  {:kino_loge, path: Path.join(root, "kino_loge")}
])

What Loge is

Loge ("logic engines") lets a notebook write problems in several logic languages and hand them to provers and solvers. Each language is its own package; this notebook installs all of them:

Every problem below sits in a Logic Engine smart cell (+ Smart → Logic Engine). From top to bottom, a cell has:

1. a language and an engine select;
2. the engine's controls, such as a time limit;
3. the editor, and under it the problems the linter finds as you type;
4. once evaluated, the outcome: a Result tab with the verdict and the details the engine reports, and an Output tab with what the engine printed.

Evaluating a cell runs ordinary Elixir. Open a cell's source (the <> toggle) to see it: one Loge.run!/3 call, which works without the smart cell installed.

Settings

Some engines need settings that hold across cells: a server, a password, the path to a binary. The Logic Engine Settings cell holds them, one engine at a time, and Verify checks that the engine can be reached. A password field takes the name of a Livebook secret, never the password itself.

None of the engines in this tour need settings if their programs are on PATH: SystemOnTPTP is a public web service; clingo and SWI-Prolog come bundled; Isabelle, z3 and cvc5 are found on PATH. If z3 lives elsewhere, set its executable here.

:ok

Proving theorems: TPTP

TPTP is the language of automated theorem provers. A cell with no engine and a variable name is a definitions cell: it holds axioms that later cells include by that name. This one defines groups:

groups =
  Loge.source(
    :tptp,
    "fof(associativity, axiom, ![X, Y, Z]: mult(mult(X, Y), Z) = mult(X, mult(Y, Z))).\nfof(left_identity, axiom, ![X]: mult(e, X) = X).\nfof(left_inverse, axiom, ![X]: mult(inv(X), X) = e).\n"
  )

A classic exercise: in a group where every element is its own inverse, multiplication commutes. The cell includes groups and asks the E prover on SystemOnTPTP. Expected: Theorem. If you edit the definitions above, this cell becomes stale, as any cell that reads a variable does.

Loge.run!(
  Loge.Tptp.Engines.SystemOnTptp,
  "include('groups').\n\nfof(self_inverse, hypothesis, ![X]: mult(X, X) = e).\nfof(commutative, conjecture, ![X, Y]: mult(X, Y) = mult(Y, X)).\n",
  system: "E",
  time_limit_sec: 10,
  includes: %{"groups" => groups}
)

Without that hypothesis, commutativity does not follow. Vampire can tell, and expected is CounterSatisfiable (or GaveUp within the time limit). The SZS status is the standard vocabulary of these verdicts; the Result tab links to its definitions.

Loge.run!(
  Loge.Tptp.Engines.SystemOnTptp,
  "include('groups').\n\nfof(commutative, conjecture, ![X, Y]: mult(X, Y) = mult(Y, X)).",
  system: "Vampire",
  time_limit_sec: 10,
  includes: %{"groups" => groups}
)

Higher-order problems (THF) can also go to Isabelle. With isabelle on PATH and no server configured, Loge starts a local Isabelle server on first use, about six seconds for the first proof, and stops it with the notebook's runtime. Each formula becomes a lemma; the table lists their statuses. Expected: Theorem for both.

Loge.run!(
  Loge.Tptp.Engines.Isabelle,
  "thf(excluded_middle, conjecture, ![P: $o]: (P | ~ P)).\nthf(drinker, conjecture, ?[X: $i]: ![Y: $i]: ((d @ X) => (d @ Y))).\nthf(d_type, type, d: $i > $o).\n",
  proof_method: "by auto"
)

Colouring a map, three ways

Can the seven regions of Australia be coloured with three colours so that no two neighbours share one? The same puzzle reads differently in each language.

In ASP, a choice rule picks one colour per region and a constraint rules out equal neighbours. clingo returns the stable models. Expected: Satisfiable, one painting. Set Models to 0 to see all 18.

Loge.run!(
  Loge.Asp.Engines.Clingo,
  "region(wa; nt; sa; q; nsw; v; t).\nborder(wa, nt). border(wa, sa). border(nt, sa). border(nt, q).\nborder(sa, q). border(sa, nsw). border(sa, v). border(q, nsw). border(nsw, v).\ncolour(red; green; blue).\n\n1 { paint(R, C) : colour(C) } 1 :- region(R).\n:- border(A, B), paint(A, C), paint(B, C).\n\n#show paint/2.\n",
  time_limit: 10
)

In SMT-LIB, each region is an integer from 1 to 3, and neighbours are distinct. z3 answers sat and the model table gives each region's number. Expected: Satisfiable. This cell needs z3 on PATH or set in the Settings cell; choose cvc5 in the engine select to use cvc5 instead.

Loge.run!(
  Loge.Smtlib.Engines.Z3,
  "(set-logic QF_LIA)\n(declare-const wa Int) (declare-const nt Int) (declare-const sa Int) (declare-const q Int)\n(declare-const nsw Int) (declare-const v Int) (declare-const t Int)\n(assert (and (<= 1 wa 3) (<= 1 nt 3) (<= 1 sa 3) (<= 1 q 3) (<= 1 nsw 3) (<= 1 v 3) (<= 1 t 3)))\n(assert (distinct wa nt)) (assert (distinct wa sa)) (assert (distinct nt sa))\n(assert (distinct nt q)) (assert (distinct sa q)) (assert (distinct sa nsw))\n(assert (distinct sa v)) (assert (distinct q nsw)) (assert (distinct nsw v))\n(check-sat)\n(get-model)\n",
  time_limit: 10
)

In Prolog, the colouring is a predicate and the question is a goal. The engine consults the program and asks the goal; the table shows the bindings of its variables, one row per answer. Expected: true, one row.

Loge.run!(
  Loge.Prolog.Engines.Swipl,
  "colour(red). colour(green). colour(blue).\n\naustralia(WA, NT, SA, Q, NSW, V, T) :-\n    maplist(colour, [WA, NT, SA, Q, NSW, V, T]),\n    WA \\== NT, WA \\== SA, NT \\== SA, NT \\== Q, SA \\== Q,\n    SA \\== NSW, SA \\== V, Q \\== NSW, NSW \\== V.\n",
  goal: "australia(WA, NT, SA, Q, NSW, V, T)",
  answers: 1,
  time_limit: 10
)

Prolog answers are not SZS statuses, so the verdict is the toplevel's: true or false. A timeout is still SZS Timeout.

Rewriting: egglog

egglog saturates an e-graph with rewrite rules and extracts the cheapest equivalent term. Here x · 1 + 0 simplifies to x. Expected: completed, the extracted term (Var "x") and, with Show the e-graph on, the e-graph: each box an e-class, holding the e-nodes found equal.

Loge.run!(
  Loge.Egglog.Engines.Egglog,
  "(datatype Math (Num i64) (Var String) (Add Math Math) (Mul Math Math))\n\n(rewrite (Add a b) (Add b a))\n(rewrite (Mul a b) (Mul b a))\n(rewrite (Add a (Num 0)) a)\n(rewrite (Mul a (Num 1)) a)\n(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))\n\n(let expr (Add (Mul (Var \"x\") (Num 1)) (Num 0)))\n(run 5)\n(extract expr)\n",
  graph: true
)

Linting as you type

Every language has a linter, run as you type. The program below has two problems: Region occurs only once in its clause (a warning, placed on the variable), and the last clause is missing a parenthesis (an error). Evaluating it raises Loge.Error naming the error; fix the clause and it runs.

Loge.run!(
  Loge.Prolog.Engines.Swipl,
  "colour(red). colour(green).\n\npaint(Region, C) :- colour(C).\npaint(wa, red :- true.\n",
  goal: "paint(wa, C)",
  answers: 0,
  time_limit: 10
)

Loge from Elixir

The smart cell is optional: everything it does is a function call. The registry knows every installed language and engine:

for language <- Loge.Registry.languages() do
  {language.id(), Enum.map(Loge.Registry.engines_for(language.id()), & &1.id())}
end

Loge.lint/3 is what runs under the editor. Each diagnostic has a code, a severity, a range in the source and a message:

Loge.lint(Loge.Smtlib.Language, "(declare-const x)\n(check-sat)", [])

Problems can also be built as data. This builds the map-colouring puzzle as a propositional formula, one variable per region and colour, for the DIMACS package. Expected: {21, 55}, 21 variables and 55 clauses.

regions = ~w(wa nt sa q nsw v t)a
borders = [wa: :nt, wa: :sa, nt: :sa, nt: :q, sa: :q, sa: :nsw, sa: :v, q: :nsw, nsw: :v]
colours = ~w(red green blue)a

variable = fn region, colour ->
  Enum.find_index(regions, &(&1 == region)) * length(colours) +
    Enum.find_index(colours, &(&1 == colour)) + 1
end

some_colour = for r <- regions, do: for(c <- colours, do: variable.(r, c))
one_colour = for r <- regions, c <- colours, d <- colours, c < d, do: [-variable.(r, c), -variable.(r, d)]
differ = for {a, b} <- borders, c <- colours, do: [-variable.(a, c), -variable.(b, c)]

cnf = %Loge.Dimacs.Cnf{
  variables: length(regions) * length(colours),
  clauses: some_colour ++ one_colour ++ differ
}

{cnf.variables, length(cnf.clauses)}

Loge.run!/3 solves it, here with clasp asked for every model, and the models decode back into paintings. Expected: {:satisfiable, 18, [...]}, Tasmania being free.

outcome = Loge.run!(Loge.Dimacs.Engines.Clasp, cnf, models: 0)
{:models, models} = List.keyfind(outcome.views, :models, 0)

paintings =
  for model <- models do
    for literal <- model, literal > 0 do
      region = Enum.at(regions, div(literal - 1, length(colours)))
      {region, Enum.at(colours, rem(literal - 1, length(colours)))}
    end
  end

{outcome.szs, length(paintings), hd(paintings)}

The Loge.Outcome holds the SZS status, the raw output and the views the Result tab draws; it renders as a cell's result does:

outcome

Where to go next

Each language has a notebook of its own beside this one (tptp.livemd, dimacs.livemd, asp.livemd, prolog.livemd, egglog.livemd, smtlib.livemd), with more cases per engine. A language or engine of your own is an Elixir module implementing Loge.Language or Loge.Engine, registered with Loge.register/1; the smart cells pick it up with no change.