Related papers: Provability in BI's Sequent Calculus is Decidable
A binary relation on graphs is recursively enumerable if and only if it can be computed by a formula in monadic second-order logic. The latter means that the formula defines a set of graphs, in the usual way, such that each "computation…
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong L\"ob logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A…
While syntactic inference restrictions don't play an important role for SAT, they are an essential reasoning technique for more expressive logics, such as first-order logic, or fragments thereof. In particular, they can result in short…
A grammar logic refers to an extension to the multi-modal logic K in which the modal axioms are generated from a formal grammar. We consider a proof theory, in nested sequent calculus, of grammar logics with converse, i.e., every modal…
The paper introduces a generalization for known probabilistic models such as log-linear and graphical models, called here multiplicative models. These models, that express probabilities via product of parameters are shown to capture…
Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent…
The field of statistical relational learning aims at unifying logic and probability to reason and learn from data. Perhaps the most successful paradigm in the field is probabilistic logic programming: the enabling of stochastic primitives…
When reasoning about formal objects whose structures involve binding, it is often necessary to analyze expressions relative to a context that associates types, values, and other related attributes with variables that appear free in the…
Logics of limited belief aim at enabling computationally feasible reasoning in highly expressive representation languages. These languages are often dialects of first-order logic with a weaker form of logical entailment that keeps reasoning…
We introduce a scalable Bayesian preference learning method for identifying convincing arguments in the absence of gold-standard rat- ings or rankings. In contrast to previous work, we avoid the need for separate methods to perform quality…
We introduce a family of comparative plausibility logics over neighbourhood models, generalising Lewis' comparative plausibility operator over sphere models. We provide axiom systems for the logics, and prove their soundness and…
Stone-type duality theorems, which relate algebraic and relational/topological models, are important tools in logic because -- in addition to elegant abstraction -- they strengthen soundness and completeness to a categorical equivalence,…
We present IBR, an Iterative Backward Reasoning model to solve the proof generation tasks on rule-based Question Answering (QA), where models are required to reason over a series of textual rules and facts to find out the related proof path…
Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cyclic proofs with traditional finite proofs: we extend abstract…
By Solovay's celebrated completeness result on formal provability we know that the provability logic $\mathrm GL$ describes exactly all provable structural properties for any sound and strong enough arithmetical theory with a decidable…
Possibilistic logic offers a qualitative framework for representing pieces of information associated with levels of uncertainty of priority. The fusion of multiple sources information is discussed in this setting. Different classes of…
The automated proof search system and decidability for logic of correlated knowledge is presented in this paper. The core of the proof system is the sequent calculus with the properties of soundness, completeness, admissibility of cut and…
We introduce and study single-conclusioned nested sequent calculi for a broad class of intuitionistic multi-modal logics known as "intuitionistic grammar logics (IGLs)." These logics serve as the intuitionistic counterparts of classical…
Even though query evaluation is a fundamental task in databases, known classifications of conjunctive queries by their fine-grained complexity only apply to queries without self-joins. We study how self-joins affect enumeration complexity,…
Sequential propositional logic deviates from ordinary propositional logic by taking into account that during the sequential evaluation of a propositional statement,atomic propositions may yield different Boolean values at repeated…