How it works

A theorem prover as a chemistry. Molecules are logical clauses, and a collision is one resolution step: if a literal in one clause and a negated literal in the other unify, the resolvent is produced. Because resolution is sound every product is a logical consequence of its parents, and because it is refutation-complete, feeding an unsatisfiable set into the reactor eventually produces the empty clause. Proof search becomes a stochastic, parallel, collision-driven process with no search strategy.

S

clauses of first-order predicate logic; species id is the canonical clause text (literals sorted, variables renamed X1, X2, ... so alphabetic variants coincide, ~ for negation, [] for the empty clause), structure the clause as 'lit | lit' · implicit

R

binary resolution (Busch 2004, Def. 1.2.12): if a literal of s1 and a negated literal of s2 have a most general unifier g, s1 + s2 -> resolvent ((s1 - {l}) u (s2 - {~l'}))g; otherwise elastic. Closure: s1 + s2 -> s1 + s2 + s3; soup, educt replacement: s1 + s2 -> s_i + s3; free replacement: s3 displaces a random molecule · arity 2

A

well-stirred-multiset · educt replacement keeps the population fixed; free replacement overwrites a random molecule; optional inflow of start clauses overwrites a random molecule (thesis algorithms 3.1-3.3)

Parameters

What to look for

• resolution is sound: every product is a logical consequence of its two reactants
• refutation-completeness: the closure of an unsatisfiable clause set contains the empty clause; a satisfiable set never produces it
• Gini (1995) example (thesis table 6.1): RESAC finds a 7-step refutation in which clauses first grow to 5 literals and then shrink to the empty clause
• the collisions needed for a proof vary strongly from run to run; with multiplicity 20 and elastic inflow most runs on table 6.1 succeed within the first 8500 collisions (thesis fig. 6.3)
• a reactor that is too small can prevent the proof; larger reactors need more collisions (thesis figs. 6.1-6.2)
• group-theory problem of table 6.2: RESAC finds a proof of length 8 in reactors of 14000 copies per clause (thesis 6.6, fig. 6.4); not reproduced at Chemart's default scale, where the closure is truncated before any refutation

Implementation decisions

• The book only sketches the idea; the chemistry is RESAC from the thesis [147]. The ECAL 2003 paper [148] (Busch & Banzhaf, How to program artificial chemistries) was not openly accessible; the thesis contains its material. Fontana & Buss [284], Howard [406] (Curry-Howard) and Nordin & Banzhaf [620] are background only: no lambda-term proof chemistry is implemented.
• First-order, as in the sources: terms with functions and constants, Robinson unification with occurs check, clauses standardised apart before resolving (Def. 1.2.12 and remark).
• Factoring (thesis 6.3 item 1, on by default) is folded into the reaction as in Robinson's original rule: the resolvents of s1 and s2 are the binary resolvents of every pair (factor of s1, factor of s2), each clause counting as its own factor. The thesis does not say how the unary factoring rule is scheduled in a binary-collision reactor.
• Identical literals always merge (clauses are sets, thesis 6.3 item 6) and tautologies are never produced (item 5). max_length (item 4) counts predicate, function, constant and variable occurrences. The per-clause limit on the number of resolutions (item 4) is not implemented: it is described only as an option and no value is published.
• Species are clauses up to variable renaming: the id renames variables in order of first occurrence and takes the lexicographically smallest text over all orderings of literals with the same variable-free skeleton. For clauses with more than 720 such orderings a single ordering is used, so a few alphabetic variants could then remain distinct species. No subsumption is applied (the thesis lists none).
• Clause syntax follows Prolog (upper-case variables, lower-case constants). Table 6.1 writes variables lower-case and the Skolem constants John, S, M upper-case; they are transcribed as X, Y, Z and john, s, m. Table 6.2's P is written p.
• Thesis table 6.1 splits the problem into s1-s5 (the theory) and s6-s8 (the negated goal: lightsleep(john), has(john,m), mice(m)); that split defines the goal clauses, which matters only for the set-of-support strategies. The extracted text of example 1.2.1 lost its negation signs; it is used in the tests with the signs restored from the prose.
• The method closure is level saturation (thesis 1.3.3 and 6.1): each round resolves every allowed pair with at least one clause from the previous round. chemart.expand.expand is not used because it allows one outcome per reactant pair, while two clauses can have several resolvents; each resolvent is a separate reaction s1 + s2 -> s1 + s2 + s3 (premises survive, the theory grows). Under set-of-support a clause is supported if any reaction producing it had a supported parent.
• The soup follows algorithms 3.1-3.3: the reactor is filled with multiplicity copies of each distinct start clause in random order; two distinct positions i != j are drawn; Res2 picks uniformly among all resolvable literal pairings (of factors), after dropping tautologies and over-long clauses. Educt replacement overwrites M[i] or M[j] with probability 1/2 (reaction s1 + s2 -> s_j + s3); free replacement overwrites a random position k, which can be one of the reactants (then recorded as s1 + s2 -> s_other + s3; otherwise s1 + s2 -> s1 + s2 + s3, the displaced molecule leaving by outflow).
• Inflow of start clauses overwrites a random molecule; it is a molecule count per collision, not a concentration rate, so it is described by parameters and extras.analysis.inflows rather than Network.inflow. The run ends at max_collisions or when the target is produced (thesis 6.3 item 7).
• The proof (extras.analysis.proof) is the list of reactions that first produced each clause on the way to the target, premises before conclusions: for the closure this is a derivation of lowest level, for the soup the actual construction pathway (book 16.5: dead ends do not appear).
• The group-theory problem (table 6.2) is provided as transcribed, but its published proof of length 8 is not checked: level saturation with 2000 species only covers levels 1-3 (about 14 s), and a soup with multiplicity 20 finds no refutation in 20000 collisions, far below the thesis's multiplicity 14000. The thesis does not list the proof steps.
• The v1 parameters axioms, target (type matrix) and max_collisions are replaced by problem/clauses/goal/target (clause text) and the soup parameters above. Rates are None: no source gives rate constants.

Sources

• Busch, J. (2004). RESAC: Eine resolutionsbasierte Kuenstliche Chemie und deren Anwendungen. PhD thesis, Universitaet Dortmund. Defs. 1.2.11-1.2.15, sec. 1.3.3, ch. 3 (eqs. 3.1-3.4, algorithms 3.1-3.3), ch. 6 (sec. 6.3, tables 6.1-6.2, figs. 6.1-6.3). https://eldorado.tu-dortmund.de/server/api/core/bitstreams/6d39161e-8d42-4b34-9398-6eeca088a148/content

Banzhaf & Yamamoto, Artificial Chemistries (2015), §16.5

Preview at default parameters

100 species · 402 reactions · status complete · seed 1

howls(X1),~dog(X1) + ~has(X1,X2),~howls(X2),~lightsleep(X1) -> howls(X1),~dog(X1) + ~has(X1,X2),~howls(X2),~lightsleep(X1) + ~dog(X1),~has(X2,X1),~lightsleep(X2)
cat(s),dog(s) + howls(X1),~dog(X1) -> cat(s),dog(s) + howls(X1),~dog(X1) + cat(s),howls(s)
has(john,s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> has(john,s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + ~cat(s),~has(john,X1),~mice(X1)
has(john,s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> has(john,s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + ~cat(X1),~has(john,X1),~mice(s)
has(john,s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> has(john,s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + ~cat(s),~mice(s)
cat(s),dog(s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> cat(s),dog(s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + dog(s),~has(X1,X2),~has(X1,s),~mice(X2)
cat(s),dog(s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> cat(s),dog(s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + dog(s),~has(X1,s),~mice(s)
has(john,m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> has(john,m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + ~cat(m),~has(john,X1),~mice(X1)
has(john,m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> has(john,m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + ~cat(X1),~has(john,X1),~mice(m)
has(john,m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> has(john,m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + ~cat(m),~mice(m)
mice(m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> mice(m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + ~cat(X1),~has(X2,X1),~has(X2,m)
mice(m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> mice(m) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + ~cat(m),~has(X1,m)
has(john,s) + ~has(X1,X2),~howls(X2),~lightsleep(X1) -> has(john,s) + ~has(X1,X2),~howls(X2),~lightsleep(X1) + ~howls(s),~lightsleep(john)
lightsleep(john) + ~has(X1,X2),~howls(X2),~lightsleep(X1) -> lightsleep(john) + ~has(X1,X2),~howls(X2),~lightsleep(X1) + ~has(john,X1),~howls(X1)
has(john,m) + ~has(X1,X2),~howls(X2),~lightsleep(X1) -> has(john,m) + ~has(X1,X2),~howls(X2),~lightsleep(X1) + ~howls(m),~lightsleep(john)
has(john,s) + ~dog(X1),~has(X2,X1),~lightsleep(X2) -> has(john,s) + ~dog(X1),~has(X2,X1),~lightsleep(X2) + ~dog(s),~lightsleep(john)
cat(s),dog(s) + ~dog(X1),~has(X2,X1),~lightsleep(X2) -> cat(s),dog(s) + ~dog(X1),~has(X2,X1),~lightsleep(X2) + cat(s),~has(X1,s),~lightsleep(X1)
lightsleep(john) + ~dog(X1),~has(X2,X1),~lightsleep(X2) -> lightsleep(john) + ~dog(X1),~has(X2,X1),~lightsleep(X2) + ~dog(X1),~has(john,X1)
has(john,m) + ~dog(X1),~has(X2,X1),~lightsleep(X2) -> has(john,m) + ~dog(X1),~has(X2,X1),~lightsleep(X2) + ~dog(m),~lightsleep(john)
dog(s),~has(X1,X2),~has(X1,s),~mice(X2) + ~dog(X1),~has(X2,X1),~lightsleep(X2) -> dog(s),~has(X1,X2),~has(X1,s),~mice(X2) + ~dog(X1),~has(X2,X1),~lightsleep(X2) + ~has(X1,X2),~has(X1,s),~has(X3,s),~lightsleep(X3),~mice(X2)
dog(s),~has(X1,X2),~has(X1,s),~mice(X2) + ~dog(X1),~has(X2,X1),~lightsleep(X2) -> dog(s),~has(X1,X2),~has(X1,s),~mice(X2) + ~dog(X1),~has(X2,X1),~lightsleep(X2) + ~has(X1,s),~has(X2,s),~lightsleep(X1),~mice(s)
dog(s),~has(X1,s),~mice(s) + ~dog(X1),~has(X2,X1),~lightsleep(X2) -> dog(s),~has(X1,s),~mice(s) + ~dog(X1),~has(X2,X1),~lightsleep(X2) + ~has(X1,s),~has(X2,s),~lightsleep(X1),~mice(s)
cat(s),howls(s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> cat(s),howls(s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + howls(s),~has(X1,X2),~has(X1,s),~mice(X2)
cat(s),howls(s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) -> cat(s),howls(s) + ~cat(X1),~has(X2,X1),~has(X2,X3),~mice(X3) + howls(s),~has(X1,s),~mice(s)
cat(s),howls(s) + ~has(X1,X2),~howls(X2),~lightsleep(X1) -> cat(s),howls(s) + ~has(X1,X2),~howls(X2),~lightsleep(X1) + cat(s),~has(X1,s),~lightsleep(X1)
cat(s),howls(s) + ~cat(s),~has(john,X1),~mice(X1) -> cat(s),howls(s) + ~cat(s),~has(john,X1),~mice(X1) + howls(s),~has(john,X1),~mice(X1)
cat(s),howls(s) + ~cat(X1),~has(john,X1),~mice(s) -> cat(s),howls(s) + ~cat(X1),~has(john,X1),~mice(s) + howls(s),~has(john,s),~mice(s)
cat(s),howls(s) + ~cat(s),~mice(s) -> cat(s),howls(s) + ~cat(s),~mice(s) + howls(s),~mice(s)
cat(s),howls(s) + ~cat(X1),~has(john,X1),~mice(m) -> cat(s),howls(s) + ~cat(X1),~has(john,X1),~mice(m) + howls(s),~has(john,s),~mice(m)
cat(s),howls(s) + ~cat(X1),~has(X2,X1),~has(X2,m) -> cat(s),howls(s) + ~cat(X1),~has(X2,X1),~has(X2,m) + howls(s),~has(X1,m),~has(X1,s)
cat(s),howls(s) + ~howls(s),~lightsleep(john) -> cat(s),howls(s) + ~howls(s),~lightsleep(john) + cat(s),~lightsleep(john)
cat(s),howls(s) + ~has(john,X1),~howls(X1) -> cat(s),howls(s) + ~has(john,X1),~howls(X1) + cat(s),~has(john,s)
has(john,s) + ~cat(s),~has(john,X1),~mice(X1) -> has(john,s) + ~cat(s),~has(john,X1),~mice(X1) + ~cat(s),~mice(s)
cat(s),dog(s) + ~cat(s),~has(john,X1),~mice(X1) -> cat(s),dog(s) + ~cat(s),~has(john,X1),~mice(X1) + dog(s),~has(john,X1),~mice(X1)
has(john,m) + ~cat(s),~has(john,X1),~mice(X1) -> has(john,m) + ~cat(s),~has(john,X1),~mice(X1) + ~cat(s),~mice(m)
mice(m) + ~cat(s),~has(john,X1),~mice(X1) -> mice(m) + ~cat(s),~has(john,X1),~mice(X1) + ~cat(s),~has(john,m)
has(john,s) + ~cat(X1),~has(john,X1),~mice(s) -> has(john,s) + ~cat(X1),~has(john,X1),~mice(s) + ~cat(s),~mice(s)
cat(s),dog(s) + ~cat(X1),~has(john,X1),~mice(s) -> cat(s),dog(s) + ~cat(X1),~has(john,X1),~mice(s) + dog(s),~has(john,s),~mice(s)
has(john,m) + ~cat(X1),~has(john,X1),~mice(s) -> has(john,m) + ~cat(X1),~has(john,X1),~mice(s) + ~cat(m),~mice(s)
cat(s),dog(s) + ~cat(s),~mice(s) -> cat(s),dog(s) + ~cat(s),~mice(s) + dog(s),~mice(s)
… 362 more

Generated by the uploader with chemart push; the hub never runs uploaded code.