We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the `precision' embedding $\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic.

We introduce a system of Hyper Natural Deduction for Gödel Logic as an extension of Gentzen’s system of Natural Deduction. A deduction in this system consists of a finite set of derivations which uses the typical rules of Natural Deduction, plus additional rules providing means for communication between derivations. We show that our system is sound and complete for infinite-valued propositional Gödel Logic, by giving translations to and from Avron’s Hypersequent Calculus. We provide conversions for normalization extending usual conversions for Natural Deduction and prove the existence of normal forms for Hyper Natural Deduction for Gödel Logic. We show that normal deductions satisfy the subformula property.

In this paper we show that a very basic fragment of FO-LTL, the monadic fully boxed fragment (all connectives and quantifiers are guarded by P) is not recursively enumerable wrt validity and 1-satisfiability if three predicates are present. This result is obtained by reduction of the fully boxed fragment of FO-LTL to the Gödel logic G↓, the infinitely valued Gödel logic with truth values in [0,1] such that all but 0 are isolated. The result on 1-satisfiability is in no way symmetric to the result on validity as in classical logic: this is demonstrated by the analysis of G↑, the related infinitely-valued Gödel logic with truth values in [0, 1] such that all but 1 are isolated. Validity of the monadic fragment with at least two predicates is not recursively enumerable, 1-satisfiability of the monadic fragment is decidable.

We introduce a Hyper Natural Deduction system as an extension of Gentzen's Natural Deduction system. A Hyper Natural Deduction consists of a finite set of derivations which may use, beside typical Natural Deduction rules, additional rules providing means for communication between derivations. We show that our Hyper Natural Deduction system is sound and complete for infinite-valued propositional Gödel Logic, by giving translations to and from Avron's Hyper sequent Calculus. We also provide conversions for normalisation and prove the existence of normal forms for our Hyper Natural Deduction system.

We consider intermediate predicate logics defined by fixed well-ordered (or dually well-ordered) linear Kripke frames with constant domains where the order-type of the well-order is strictly smaller than ωω. We show that two such logics of different order-type are separated by a first-order sentence using only one monadic predicate symbol. Previous results by Minari, Takano and Ono, as well as the second author, obtained the same separation but relied on the use of predicate symbols of unbounded arity.

Open source software (OSS) or Free/Libre OSS (FLOSS) has become an interesting source of research in software engineering. However, it has been criticized that FLOSS development is often considered as a homogeneous phenomenon grounded by assumptions rather than empirical evidence. Proper empirical methods that can shed light into FLOSS development are desirable. In this paper, we propose an empirical method to validate a software development model for FLOSS, the Adapted Staged Model for FLOSS. We mined some selected metrics from Apache Ivy and study their evolution using S-shaped curves. Our results indicate that S-shaped curves can model software evolution well for Ivy. Moreover, we demonstrated that our method can be used to identify successfully different stages of its development, validating part of the Adapted Staged Model for FLOSS.

The minimal extension of intuitionistic propositional language is characterized, where propositional quantifiers are eliminable w.r.t. Kripke frames of type ω.

Abstract We investigate the relation between intermediate predicate logics based on countable linear Kripke frames with constant domains and Gödel logics. We show that for any such Kripke frame there is a Gödel logic which coincides with the logic defined by this Kripke frame on constant domains and vice versa. This allows us to transfer several recent results on Gödel logics to logics based on countable linear Kripke frames with constant domains: We obtain a complete characterisation of axiomatisability of logics based on countable linear Kripke frames with constant domains. Furthermore, we obtain that the total number of logics defined by countable linear Kripke frames on constant domains is countable.