Searcharxiv⌕ Search

arXiv subjects

Edward Hermann Haeusler

Publications and source records attributed to Edward Hermann Haeusler.

At least 19 recordsLinked to original sources
arXiv2026

The Free Inference Dimension: Complexity Measure for Zero-Collision Navigation under Hypothesis Mixtures

Solomonoff induction frames prediction as a mixture over computable hypotheses, typically leading to identification of the true environment. In a finite meta-reinforcement learning setting with nested constraint families, in our previous work, we observe a different regime: a value-mixture (VM) agent achieves near-optimal, zero-collision navigation without identifying the true environment, a phenomenon we call Free Inference. This regime persists up to a sharp density threshold, beyond which performance degrades and posterior-mode selection (PMS) becomes preferable. We formalize this behavior via the Free Inference dimension dFI(S,N), a combinatorial measure of the environmental complexity a VM agent can handle while preserving trajectory coherence. We prove dFI is strictly smaller than the VC-dimension and relates to the Natarajan dimension up to a path-length factor, capturing the cost of non-decomposable loss. A PAC-style relaxation yields generalization bounds driven by dFI^(epsilon,delta). We also define a complementary PMS identification dimension and show that a hybrid strategy---averaging until the first collision, then switching to selection---is optimal, with links to Littlestone-type dimensions supported by grid-world experiments.

cs.LG↗
arXiv2026

From Dag-Like Proofs to Boolean Circuits in Lean

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 minimal logic, as Boolean circuits. These DLDS compress Natural Deduction tree-like proofs into directed acyclic graphs, preserving logical correctness while reducing redundancy. We formally define the circuit construction process and establish its pointwise correctness, showing that, for any fixed path assignment, the resulting Boolean circuit agrees with the intended dependency-propagation semantics. A Lean formalization establishes machine-checked guarantees for the circuit evaluator and includes a restricted bridge for the uncompressed simple-tree fragment, connecting valid DLDS instances in that fragment to genuine circuit acceptance of their extracted paths under the route and discharge conditions formalized in Lean. This approach opens new perspectives for automated theorem proving and formal certification.

cs.LO↗
arXiv2026

A note on Jerabek's paper "A simplified lower bound for implicational logic"

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 Prawitz's Natural Deduction (ND) for implicational minimal logic with references to Hudelmaier's cutfree sequent calculus. In this note we comment on Jeřábek's approach that claimed to refute our results by providing exponential lower bounds on the implicational minimal logic. This claim is wrong and misleading, which is briefly demonstrated by Basis example below.

cs.CC↗
arXiv2025

On the horizontal compression of dag-derivations in minimal purely implicational logic

This report defines (plain) Dag-like derivations in the purely implicational fragment of minimal logic $M_{\supset}$. Introduce the horizontal collapsing set of rules and the algorithm {\bf HC}. Explain why {\bf HC} can transform any polynomial height-bounded tree-like proof of a $M_{\supset}$ tautology into a smaller dag-like proof. Sketch a proof that {\bf HC} preserves the soundness of any tree-like ND in $M_{\supset}$ in its dag-like version after the horizontal collapsing application. We show some experimental results about applying the compression method to a class of (huge) propositional proofs and an example, with non-hamiltonian graphs, for qualitative analysis. The contributions include the comprehensive presentation of the set of horizontal compression (HC), the (sketch) of the proof that HC rules preserve soundness and the demonstration that the compressed dag-like proofs are polynomially upper-bounded when the submitted tree-like proof is height and foundation poly-bounded. Finally, in the appendix, we outline an algorithm that verifies in polynomial time on the size of the dag-like proofs whether they are valid proofs of their conclusions.In the conclusion we discuss what part of the formal results on the HC-compressed dag-like proofs have been proved with the use of Interactive Theorem Prover assistance.

cs.LO↗
arXiv2023

Quantum Algorithm for Multiplicative Linear Logic

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 Algorithm and Linear Logic, show the detailed steps of the algorithm and then present the results obtained on quantum simulators.

cs.LO↗
arXiv2021

A logical framework with a graph meta-language

We conjecture that the relative unpopularity of logical frameworks among practitioners is partly due to their complex meta-languages, which often demand both programming skills and theoretical knowledge of the meta-language in question for them to be fruitfully used. We present ongoing work on a logical framework with a meta-language based on graphs. A simpler meta-language leads to a shallower embedding of the object language, but hopefully leads to easier implementation and usage. A graph-based logical framework also opens up interesting possibilities in time and space performance by using heavily optimized graph databases as backends and by proof compression algorithms geared towards graphs. Deductive systems can be specified using simple domain-specific languages built on top of the graph database's query language. There is support for interactive (through a web-based interface) and semiautomatic (following user-defined tactics specified by a domain-specific language) proof modes. We have so far implemented nine systems for propositional logic, including Fitch-style and backward-directed Natural Deduction systems for intuitionistic and classical logic (with the classical systems reusing the rules of the intuitionistic ones), and a Hilbert-style system for the K modal logic.

cs.LO↗
arXiv2021

On the Intrinsic Redundancy in Huge Natural Deduction proofs II: Analysing $M_{\imply}$ Super-Polynomial Proofs

This article precisely defines huge proofs within the system of Natural Deduction for the Minimal implicational propositional logic \mil. This is what we call an unlimited family of super-polynomial proofs. We consider huge families of expanded normal form mapped proofs, a device to explicitly help to count the E-parts of a normal proof in an adequate way. Thus, we show that for almost all members of a super-polynomial family there at least one sub-proof or derivation of each of them that is repeated super-polynomially many times. This last property we call super-polynomial redundancy. Almost all, precisely means that there is a size of the conclusion of proofs that every proof with conclusion bigger than this size and that is huge is highly redundant too. This result points out to a refinement of compression methods previously presented and an alternative and simpler proof that CoNP=NP.

cs.LO↗
arXiv2021

Going from the huge to the small: Efficient succinct representation of proofs in Minimal implicational logic

A previous article shows that any linear height bounded normal proof of a tautology in the Natural Deduction for Minimal implicational logic $M_{\supset}$ is as huge as it is redundant. More precisely, any proof in a family of super-polynomially sized and linearly height bounded proofs have a sub-derivation that occurs super-polynomially many times in it. In this article, we show that by collapsing all the repeated sub-derivations we obtain a smaller structure, a rooted Directed Acyclic Graph (r-DAG), that is polynomially upper-bounded on the size of $α$ and it is a certificate that $α$ is a tautology that can be verified in polynomial time. In other words, for every huge proof of a tautology in $M_{\supset}$, we obtain a succinct certificate for its validity. Moreover, we show an algorithm able to check this validity in polynomial time on the certificate's size. Comments on how the results in this article are related to a proof of the conjecture $NP=CoNP$ appears in conclusion.

cs.CC↗
arXiv2020

Yet another argument in favour of NP=CoNP

This article shows yet another proof of NP=CoNP$. In a previous article, we proved that NP=PSPACE and from it we can conclude that NP=CoNP immediately. The former proof shows how to obtain polynomial and, polynomial in time checkable Dag-like proofs for all purely implicational Minimal logic tautologies. From the fact that Minimal implicational logic is PSPACE-complete we get the proof that NP=PSPACE. This first proof of NP=CoNP uses Hudelmaier linear upper-bound on the height of Sequent Calculus minimal implicational logic proofs. In an addendum to the proof of NP=PSPACE, we observe that we do not need to use Hudelmaier upper-bound since any proof of non-hamiltonicity for any graph is linear upper-bounded. By the CoNP-completeness of non-hamiltonicity, we obtain NP=CoNP as a corollary of the first proof. In this article we show the third proof of CoNP=NP, also providing polynomial size and polynomial verifiable certificates that are Dags. They are generated from normal Natural Deduction proofs, linear height upper-bounded too, by removing redundancy, i.e., repeated parts. The existence of repeated parts is a consequence of the redundancy theorem for a family of super-polynomial proofs in the purely implicational Minimal logic. It is mandatory to read at least two previous articles to get the details of the proof presented here. The article that proves the redundancy theorem and the article that shows how to remove the repeated parts of a normal Natural Deduction proof to have a polynomial Dag certificate for minimal implicational logic tautologies.

cs.CC↗
arXiv2020

Exponentially Huge Natural Deduction proofs are Redundant: Preliminary results on $M_\supset$

We estimate the size of a labelled tree by comparing the amount of (labelled) nodes with the size of the set of labels. Roughly speaking, a exponentially big labelled tree, is any labelled tree that has an exponential gap between its size, number of nodes, and the size of its labelling set. The number of sub-formulas of any formula is linear on the size of it, and hence any exponentially big proof has a size $a^n$, where $a>1$ and $n$ is the size of its conclusion. In this article, we show that the linearly height labelled trees whose sizes have an exponential gap with the size of their labelling sets posses at least one sub-tree that occurs exponentially many times in them. Natural Deduction proofs and derivations in minimal implicational logic ($M_\supset$) are essentially labelled trees. By the sub-formula principle any normal derivation of a formula $α$ from a set of formulas $Γ=\{γ_1,\ldots,γ_n\}$ in $M_\supset$, establishing $Γ\vdash_{M_\supset}α$, has only sub-formulas of the formulas $α,γ_1,\ldots,γ_n$ occurring in it. By this relationship between labelled trees and derivations in $M_\supset$, we show that any normal proof of a tautology in $M_\supset$ that is exponential on the size of its conclusion has a sub-proof that occurs exponentially many times in it. Thus, any normal and linearly height bounded proof in $M_\supset$ is inherently redundant. Finally, we briefly discuss how this redundancy provides us with a highly efficient compression method for propositional proofs. We also provide some examples that serve to convince us that exponentially big proofs are more frequent than one can imagine.

cs.LO↗
arXiv2020

A Sequent Calculus Proof Search Procedure and Counter-model Generation based on Natural Deduction Bounds

In a previously published ENTCS paper (Santos et al. (2016)), we introduced a sequent calculus called $\mathbf{LMT^{\rightarrow}}$ for Minimal Implicational Propositional Logic ($\mathbf{LMT^{\rightarrow}}$). This calculus provides a proof search procedure for $\mathbf{LMT^{\rightarrow}}$ that works in a bottom-up approach. We proved there that $\mathbf{LMT^{\rightarrow}}$ is sound and complete. We also suggested a strategy to guarantee termination of the proof search procedure. In this current paper, we refined this strategy and presented a new strategy for $\mathbf{LMT^{\rightarrow}}$ termination. Considering this new strategy, we also provide a (new) completeness proof for the system, which improves the previous version. Besides that, we present explicit upper bounds on the proof search procedure, derived from this new strategy. We also provide a full soundness proof of the system.

cs.LO↗
arXiv2018

Modeling Normative Multi-Agent Systems from a Kelsenian Perspective

Standard Deontic Logic (SDL) has been used as the underlying logic to model and reason over Multi-Agent Systems governed by norms (NorMAS). It is known that SDL is not able to represent contrary-to-duty (CTD) scenarios in a consistent way. That is the case, for example, of the so-called Chisholm paradox, which models a situation in which a conditional obligation that specifies what must be done when a primary obligation is violated holds. In SDL, the set of sentences that represent the Chisholm paradox derives inconsistent sentences. Due to the autonomy of the software agents of a NorMAS, norms may be violated and the underlying logic used to model the NorMAS should be able to represent violation scenarios. The contribution of this paper is threefold: (i) we present how Kelsenian thinking, from his jurisprudence in the context of legal ontologies, and Intuitionist Hybrid Logic can be adopted in the modeling of NorMAS, (ii) discuss how this approach overcomes limitations of the SDL and (iii) present a discussion about normative conflict identification according to Hill's functional taxonomy, that generalizes from standard identification by impossibility-of-joint-compliance test.

cs.LO↗
arXiv2018

On How Kelsenian Jurisprudence and Intuitionistic Logic help to avoid Contrary-to-Duty paradoxes in Legal Ontologies

In this article we show how Hans Kelsen jurisprudence and Intuitionistic logic are used to avoid the well-known contrary-to-duty (CTD) paradoxes, such as Chisholm paradoxes and its variants. This article uses an intuitionistic version of the ALC description logic, named iALC, to show how an ontology based on individually valid legal statements is able to avoid CTDs by providing models to them.

cs.LO↗
arXiv2017

Passing the Brazilian OAB Exam: data preparation and some experiments

In Brazil, all legal professionals must demonstrate their knowledge of the law and its application by passing the OAB exams, the national bar exams. The OAB exams therefore provide an excellent benchmark for the performance of legal information systems since passing the exam would arguably signal that the system has acquired capacity of legal reasoning comparable to that of a human lawyer. This article describes the construction of a new data set and some preliminary experiments on it, treating the problem of finding the justification for the answers to questions. The results provide a baseline performance measure against which to evaluate future improvements. We discuss the reasons to the poor performance and propose next steps.

cs.CL↗
arXiv2016

NP vs PSPACE

We present a proof of the conjecture $\mathcal{NP}$ = $\mathcal{PSPACE}$ by showing that arbitrary tautologies of Johansson's minimal propositional logic admit "small" polynomial-size dag-like natural deductions in Prawitz's system for minimal propositional logic. These "small" deductions arise from standard "large"\ tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying "geometric" idea: if the height, $h\left( \partial \right) $ , and the total number of distinct formulas, $ϕ\left( \partial \right) $ , of a given tree-like deduction $\partial$ of a minimal tautology $ρ$ are both polynomial in the length of $ρ$, $\left| ρ\right|$, then the size of the horizontal dag-like compression is at most $h\left( \partial \right) \times ϕ\left( \partial \right) $, and hence polynomial in $\left| ρ\right|$. The attached proof is due to the first author, but it was the second author who proposed an initial idea to attack a weaker conjecture $\mathcal{NP}= \mathcal{\mathit{co}NP}$ by reductions in diverse natural deduction formalisms for propositional logic. That idea included interactive use of minimal, intuitionistic and classical formalisms, so its practical implementation was too involved. The attached proof of $ \mathcal{NP}=\mathcal{PSPACE}$ runs inside the natural deduction interpretation of Hudelmaier's cutfree sequent calculus for minimal logic.

cs.CC↗
arXiv2016

Finiteness and Computation in Toposes

Some notions in mathematics can be considered relative. Relative is a term used to denote when the variation in the position of an observer implies variation in properties or measures on the observed object. We know, from Skolem theorem, that there are first-order models where the set of real numbers is countable and some where it is not. This fact depends on the position of the observer and on the instrument/language the obserevr uses as well, i.e., it depends on whether he/she is inside the model or not and in this particular case the use of first-order logic. In this article, we assume that computation is based on finiteness rather than natural numbers and discuss Turing machines computable morphisms defined on top of the sole notion finiteness. We explore the relativity of finiteness in models provided by toposes where the Axiom of Choice (AC) does not hold, since Tarski proved that if AC holds then all finiteness notions are equivalent. Our toposes do not have natural numbers object (NNO) either, since in a topos with a NNO these finiteness notions are equivalent to Peano finiteness going back to computation on top of Natural Numbers. The main contribution of this article is to show that although from inside every topos, with the properties previously stated, the computation model is standard, from outside some of these toposes, unexpected properties on the computation arise, e.g., infinitely long programs, finite computations containing infinitely long ones, infinitely branching computations. We mainly consider Dedekind and Kuratowski notions of finiteness in this article.

cs.LO↗