Search

Join-preserving maps on the discrete time scale ω+, referred to as time warps, have been proposed as graded modalities that can be used to quantify the growth of information in the course of program execution. The set of time warps forms a simple distributive involutive residuated lattice--called the time warp algebra--that is equipped with residual operations relevant to potential applications. In this paper, we show that although the time warp algebra generates a variety that lacks the finite model property, it nevertheless has a decidable equational theory. We also describe an implementation of a procedure for deciding equations in this algebra, written in the OCaml programming language, that makes use of the Z3 theorem prover. [ABSTRACT FROM AUTHOR]

Nitrate and nitrite reduction to ammonia and nitrous oxide by anaerobic E. coli batch cultures is investigated by advanced spectroscopic analytical techniques with 15N-isotopic labelling. Non-invasive, in situ analysis of the headspace is achieved using White cell FTIR and cavity-enhanced Raman (CERS) spectroscopies alongside liquid-phase Raman spectroscopy. For gas-phase analysis, White cell FTIR measures CO2, ethanol and N2O while CERS allows H2, N2 and O2 monitoring. The 6 m pathlength White cell affords trace gas detection of N2O with a noise equivalent detection limit of 60 nbar or 60 ppbv in 1 atm. Quantitative analysis is discussed for all four 14N/15N-isotopomers of N2O. Monobasic and dibasic phosphates, acetate, formate, glucose and NO3− concentrations are obtained by liquid-phase Raman spectroscopy, with a noise equivalent detection limit of 0.6 mM for NO3− at 300 s integration time. Concentrations of the phosphate anions are used to calculate the pH in situ using a modified Henderson–Hasselbalch equation. NO2− concentrations are determined by sampling for colorimetric analysis and NH4+ by basifying samples to release 14N/15N-isotopomers of NH3 for measurement in a second FTIR White cell. The reductions of 15NO3−, 15NO2−, and mixed 15NO3− and 14NO2− by anaerobic E. coli batch cultures are discussed. In a major pathway, NO3− is reduced to NH4+via NO2−, with the bulk of NO2− reduction occurring after NO3− depletion. Using isotopically labelled 15NO3−, 15NH4+ production is distinguished from background 14NH4+ in the growth medium. In a minor pathway, NO2− is reduced to N2O via the toxic radical NO. With excellent detection sensitivities, N2O serves as a monitor for trace NO2− reduction, even when cells are predominantly reducing NO3−. The analysis of N2O isotopomers reveals that for cultures supplemented with mixed 15NO3− and 14NO2− enzymatic activity to reduce 14NO2− occurs immediately, even before 15NO3− reduction begins. Optical density and pH measurements are discussed in the context of acetate, formate and CO2 production. H2 production is repressed by NO3−; but in experiments with NO2− supplementation only, CERS detects H2 produced by formate disproportionation after NO2− depletion. [ABSTRACT FROM AUTHOR]

This article presents a new method for obtaining small algebras to check the admissibility—equivalently, validity in free algebras—of quasi-identities in a finitely generated quasivariety. Unlike a previous algebraic approach of Metcalfe and Röthlisberger, which is feasible only when the relevant free algebra is not too large, this method exploits natural dualities for quasivarieties to work with structures of smaller cardinality and surjective rather than injective morphisms. A number of case studies are described here that could not be be solved using the algebraic approach, including (quasi)varieties of MS-algebras, double Stone algebras, and involutive Stone algebras. [ABSTRACT FROM AUTHOR]

A many-valued modal logic is introduced that combines the usual Kripke frame semantics of the modal logic K with connectives interpreted locally at worlds by lattice and group operations over the real numbers. A labelled tableau system is provided and a coNEXPTIME upper bound obtained for checking validity in the logic. Focussing on the modal-multiplicative fragment, the labelled tableau system is then used to establish completeness for a sequent calculus that admits cut-elimination and an axiom system that extends the multiplicative fragment of Abelian logic. [ABSTRACT FROM AUTHOR]

Axiomatic bases of admissible rules are obtained for fragments of the substructural logic R-mingle. In particular, it is shown that a 'modus-ponens-like' rule introduced by Arnon Avron forms a basis for the admissible rules of its implication and implication-fusion fragments, while a basis for the admissible rules of the full multiplicative fragment requires an additional countably infinite set of rules. Indeed, this latter case provides an example of a three-valued logic with a finitely axiomatizable consequence relation that has no finite basis for its admissible rules. [ABSTRACT FROM AUTHOR]

A new hierarchy of "exact" unification types is introduced, motivated by the study of admissible rules for equational classes and non-classical logics. In this setting, unifiers of identities in an equational class are preordered, not by instantiation, but rather by inclusion over the corresponding sets of unified identities. Minimal complete sets of unifiers under this new preordering always have a smaller or equal cardinality than those provided by the standard instantiation preordering, and in significant cases a dramatic reduction may be observed. In particular, the classes of distributive lattices, idempotent semigroups, and MV-algebras, which all have nullary unification type, have unitary or finitary exact type. These results are obtained via an algebraic interpretation of exact unification, inspired by Ghilardi's algebraic approach to equational unification. [ABSTRACT FROM AUTHOR]

The Craig interpolation property is investigated for substructural logics whose algebraic semantics are varieties of semilinear (subdirect products of linearly ordered) pointed commutative residuated lattices. It is shown that Craig interpolation fails for certain classes of these logics with weakening if the corresponding algebras are not idempotent. A complete characterization is then given of axiomatic extensions of the 'R-mingle with unit' logic (corresponding to varieties of Sugihara monoids) that have the Craig interpolation property. This latter characterization is obtained using a model-theoretic quantifier elimination strategy to determine the varieties of Sugihara monoids admitting the amalgamation property. [ABSTRACT FROM AUTHOR]

An approximate Herbrand theorem is established for first-order infinite-valued Łukasiewicz Logic and used to obtain a proof-theoretic proof of Skolemization. These results are then used to define proof systems in the framework of hypersequents. In particular, a calculus lacking cut elimination is defined for the first-order logic characterized by linearly ordered MV-algebras, a cut-free calculus with an infinitary rule for the full first-order Łukasiewicz Logic, and a cut-free calculus with finitary rules for its one-variable fragment. [ABSTRACT FROM PUBLISHER]

Comparative logics were introduced by Casari in the 1980s to treat aspects of comparative reasoning occurring in natural language. In this article Gentzen systems are defined for these logics by means of a special mix rule that combines calculi for various substructural logics with a hypersequent calculus for Meyer and Slaney's Abelian logic. Cut-elimination is established for all these systems, and as a consequence, a positive answer is given to an open problem on the decidability of the basic comparative logic. [ABSTRACT FROM PUBLISHER]

We present logic programming style “goal-directed” proof methods for Łukasiewicz logic Ł that both have a logical interpretation, and provide a suitable basis for implementation. We introduce a basic version, similar to goal-directed calculi for other logics, and make refinements to improve efficiency and obtain termination. We then provide an algorithm for fuzzy logic programming in Rational Pavelka logic RPL, an extension of Ł with rational constants. [ABSTRACT FROM PUBLISHER]

Presents two embeddings of Łukasiewicz logic into Meyer and Slaney's Abelian logic, the logic of lattice-ordered Abelian groups. Analytic proof systems for Abelian logic; Use of the embeddings to derive corresponding systems for Lukasiewicz logic; Implications on studies of computational logic.

A biography of Bavarian Jewish blue-collar worker Herman Ickelheimer. Born in 1824, he learned the trade of a house painter which he pursued until the discovery of gold led him to seek his fortune on the shores of the Pacific. He became a member of the Volunteer Fire Department and belonged to St. Francis Hook and Ladder Company. He was married to Pauline Nordheim in 1858. He passed away in the presence of relatives on January 7, 1888 at the age of 64.

The article discusses reports published in the October 2011 issue of the "Journal of Logic & Computation," devoted to mathematical fuzzy logic, including papers that address syntactic issues for Gödel-Dummett logic.

The article discusses various reports published within the issue, including one on constructive logic with strong negation and its corresponding variety of Nelson algebras, another on the relationship between the logical property of interpolation and the algebraic property of amalgamation, as well as a report on a framework for investigating certain fragments of English that extend syllogistic logics with verbs and certain types of noun phrases.

The article introduces a report by Petr Cintula and Petr Hájek which discusses ¿ukasiewicz logic.