17 citations · 42 across the 27 of their papers we have counts for
28 papers
From Dag-Like Proofs to Boolean Circuits in Lean
Lorenzo Saraiva, Edward Hermann Haeusler
In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), obtained via horizontal compression of Natural Deduction proofs in purely implicational m…
A note on Jerabek's paper "A simplified lower bound for implicational logic"
Lev Gordeev, Edward Hermann Haeusler
In our previous papers we sketched proofs of the equality NP = coNP = PSPACE. These results have been obtained by proof theoretic tree-to-dag compressing techniques adapted to Praw…
Proofs of NP = coNP = PSPACE: Current upgrade
Lev Gordeev, Edward Hermann Haeusler
In this paper we present a more transparent upgrade of our proofs and comment on Jerabek's paper [8].
Quantum Algorithm for Multiplicative Linear Logic
Lorenzo Saraiva, Edward Hermann Haeusler, Vaston Costa
This paper describes a quantum algorithm for proof search in sequent calculus of a subset of Linear Logic using the Grover Search Algorithm. We briefly overview the Grover Search A…
On the horizontal compression of dag-derivations in minimal purely implicational logic
Edward Hermann Haeusler, José Flávio Cavalcante Barros Junior, Robinson
This report defines (plain) Dag-like derivations in the purely implicational fragment of minimal logic . Introduce the horizontal collapsing set of rules and the algor…
On proof theory in computational complexity: overview
L. Gordeev, E. H. Haeusler
In [GH1] and [GH2] (see also [GH3]) we presented full proof of the equalities NP = coNP = PSPACE. These results have been obtained by the novel proof theoretic tree-to-dag compress…