BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Edward Hermann Haeusler

Edward Hermann Haeusler appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceComputational Complexity

Catalog footprint

What is connected

12works
2topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

12 published item(s)

preprint2021arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Every super-polynomial proof in purely implicational minimal logic has a polynomially sized proof in classical implicational propositional logic

In this article we show how any formula A with a proof in minimal implicational logic that is super-polynomially sized has a polynomially-sized proof in classical implicational propositional logic . This fact provides an argument in favor that any classical propositional tautology has short proofs, i.e., NP=CoNP.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Propositional Logics Complexity and the Sub-Formula Property

In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic (M-imply) is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Goedel translation from S4 into Intuitionistic Logic, the PSPACE- completeness of M-imply is drawn. The sub-formula principle for a deductive system for a logic L states that whenever F1,...,Fk proves A, there is a proof in which each formula occurrence is either a sub-formula of A or of some of Fi. In this work we extend Statman result and show that any propositional (possibly modal) structural logic satisfying a particular formulation of the sub-formula principle is in PSPACE. If the logic includes the minimal purely implicational logic then it is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME. We also show how our technique can be used to prove that any finitely many-valued logic has the set of its tautologies in PSPACE.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

An Intuitionisticaly based Description Logic

This article presents iALC, an intuitionistic version of the classical description logic ALC, based on the framework for constructive modal logics presented by Simpson \cite{simpson95} and related to description languages, via hybrid logics, by dePaiva \cite{depaiva2003}. This article correcta and extends the presentation of iALC appearing in \cite{PHR:2010}. It points out the difference between iALC and the intuitionistic hybrid logic presented in \cite{depaiva2003}. Completeness and soundness proofs are provided. A brief discussion on the computacional complexity of iALC provability is taken. It is worth mentioning that iALC is used to formalize legal knowledge \cite{HPR:2010a,HPR:2010ab,Jurix, HPR:2011}, and in fact, was specifically designed to this goal.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

How many times do we need and assumption ?

In this article we present a class of formulas Fn, n in Nat, that need at least 2^n assumptions to be proved in a normal proof in Natural Deduction for purely implicational minimal propositional logic. In purely implicational classical propositional logic, with Peirce's rule, each Fn is proved with only one assumption in Natural Deduction in a normal proof. Hence, the formulas Fn have exponentially sized proofs in cut-free Sequent Calculus and Tableaux. In fact 2^n is the lower-bound for normal proofs in ND, cut-free Sequent proofs and Tableaux. We discuss the consequences of the existence of this class of formulas for designing automatic proof-procedures based on these deductive systems.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Proof-graphs for Minimal Implicational Logic

It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. The aim of this work is to study how to reduce the weight of propositional deductions. We present the formalism of proof-graphs for purely implicational logic, which are graphs of a specific shape that are intended to capture the logical structure of a deduction. The advantage of this formalism is that formulas can be shared in the reduced proof. In the present paper we give a precise definition of proof-graphs for the minimal implicational logic, together with a normalization procedure for these proof-graphs. In contrast to standard tree-like formalisms, our normalization does not increase the number of nodes, when applied to the corresponding minimal proof-graph representations.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Reasoning about Games via a First-order Modal Model Checking Approach

In this work, we present a logic based on first-order CTL, namely Game Analysis Logic (GAL), in order to reason about games. We relate models and solution concepts of Game Theory as models and formulas of GAL, respectively. Precisely, we express extensive games with perfect in- formation as models of GAL, and Nash equilibrium and subgame perfect equilibrium by means of formulas of GAL. From a practical point of view, we provide a GAL model checker in order to analyze games automatically. We use our model checker in at least two directions: to find solution con- cepts of Game Theory; and, to analyze players that are based on standard algorithms of the AI community, such as the minimax procedure.

0 citations0 reviewsNo code linkedOpen access