On generating large classes of Sheffer functions.
On global induction mechanisms in a -calculus with explicit approximations
We investigate a Gentzen-style proof system for the first-order -calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...
On global induction mechanisms in a μ-calculus with explicit approximations
We investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...
On guessing whether a sequence has a certain property.
On hidden variables
On ideals in De Morgan residuated lattices
In this paper, we introduce a new class of residuated lattices called De Morgan residuated lattices, we show that the variety of De Morgan residuated lattices includes important subvarieties of residuated lattices such as Boolean algebras, MV-algebras, BL-algebras, Stonean residuated lattices, MTL-algebras and involution residuated lattices. We investigate specific properties of ideals in De Morgan residuated lattices, we state the prime ideal theorem and the pseudo-complementedness of the ideal...
On independent recursive axiomatisation in intuitionistic logic
On information storage and retrieval systems
On interpolation when function symbols are present.
On interpretability in set theories. II.
On interpretability in theories containing arithmetic
On interpretability in theories containing arithmetic. II.
On Intuitionistic Sentential Connectives I.
On knowledge games.
We give a formalization of the ?knowledge games? which allows to study their decidability and convergence as a problem of mathematics. Our approach is based on a metalemma analogous to those of Von Neumann and Morgenstern at the beginning of Game Theory. We are led to definitions which characterize the knowledge games as objects is standard set theory. We then study rigorously the most classical knowledge games and, although we also prove that the ?common knowledge? in these games may be incomputable,...
On Lamport's comparison between linear and branching time temporal logic
On local proof restrictions for strong theories [Book]
On logical fiberings and automated deduction in many-valued logics using Gröbner bases.
The concept of logical fiberings is briefly summarized. Based on experiences with concrete examples an algorithmic approach is developed which leads to a represention of a many-valued logic as a logical fibering. The Stone isomorphism for expressing classical logical operations by corresponding polynomials can be extended to m-valued logics. On the basis of this, a classical deduction problem can be treated symbolically as a corresponding ideal membership problem using computer algebra support with...
On logical wholeness of an (axiomatic) formal theory
On Markov Properties Of Finitely Presented Groups
On Markov properties of finitely presented groups.