22 citations · 40 across the 13 of their papers we have counts for
15 papers
Combinatorial Proofs and Decomposition Theorems for First-order Logic
Dominic Hughes, Lutz Straßburger, Jui-Hsuan Wu
We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof sy…
First-order proofs without syntax
Dominic J. D. Hughes
Proofs are traditionally syntactic, inductively generated objects. This paper reformulates first-order logic (predicate calculus) with proofs which are graph-theoretic rather than…
Unification nets: canonical proof net quantifiers
Dominic J. D. Hughes
Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redund…
MALL proof nets identify proofs modulo rule commutation
Rob van Glabbeek, Dominic Hughes
We show that the proof nets introduced in [Hughes & van Glabbeek 2003, 2005] for MALL (Multiplicative Additive Linear Logic, without units) identify cut-free proofs modulo rule com…
Is Wolfram and Cook's (2,5) Turing machine really universal?
Dominic J. D. Hughes
Wolfram [2, p. 707] and Cook [1, p. 3] claim to prove that a (2,5) Turing machine (2 states, 5 symbols) is universal, via a universal cellular automaton known as Rule 110. The firs…
Linking diagrams for free
Dominic J. D. Hughes
Linking diagrams with path composition are ubiquitous, for example: Temperley-Lieb and Brauer monoids, Kelly-Laplaza graphs for compact closed categories, and Girard's multiplicati…