We introduce a path-based cyclic proof system for first-order $\mu $-calculus, the extension of first-order logic by second-order quantifiers for least and greatest fixed points of definable monotone functions. We prove soundness of the system and demonstrate it to be as expressive as the known trace-based cyclic systems of Dam and Sprenger. Furthermore, we establish cut-free completeness of our system for the fragment corresponding to the modal $\mu $-calculus.

Wie entstand die besondere Ermächtigung des Menschen zur Gestaltung von Geschichte und Zukunft? Ist der Gedanke der 'Machbarkeit' nicht sogar Ausgangspunkt der neuzeitlichen Wende? In welcher Kontinuität stehen die autoritär-ideologischen oder völkischfaschistischen Gesellschaftsideologien des 20. Jahrhunderts? Welche Visionen werden in der Globalisierungsdebatte erörtert? Die Vorstellung einer grundsätzlichen Gestaltbarkeit gesellschaftlicher Wirklichkeit scheint ein spezifisches Kennzeichen moderner Gesellschaften zu sein. Ein Kennzeichen, das bisher wenig hinterfragt ist. Eine besondere Herausforderung sucht dieser interdisziplinär angelegte Band, indem er zur Diskussion stellt, inwieweit der politische (...) Plan, eine radikal veränderte Zukunft für eine nächste Generation schaffen zu wollen, gesellschaftliche Gewaltprozesse akzeptiert und legitimiert. (shrink)

The larger project broached here is to look at the generally sentence “if X is well-ordered then f is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory Tf whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, (...) we prove in this paper that the statement “if X is well-ordered then εX is well-ordered” is equivalent to . This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a fragment of. (shrink)

The article shows a simple way of calibrating the strength of the theory of positive induction, ${{\rm ID}^{*}_{1}}$ . Crucially the proof exploits the equivalence of ${\Sigma^{1}_{1}}$ dependent choice and ω-model reflection for ${\Pi^{1}_{2}}$ formulae over ACA 0. Unbeknown to the authors, D. Probst had already determined the proof-theoretic strength of ${{\rm ID}^{*}_{1}}$ in Probst, J Symb Log, 71, 721–746, 2006.

We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded (...) proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations. (shrink)

Building design based on principles of architecture in harmony with the climate of each region, in addition to creating thermal comfort in building interiors, reduces fuel consumption and more important it will demonstrate a clean and green environment. This issue becomes more intense in some geological areas like Khoramshahr in Iran, which has a warm, tropical and critical climate, since if this issue is not taking into account, using air conditioning utilities would be necessary in most periods of the year. (...) According to the studies, buildings in harmony with the climate of Khorramshahr will be able to adjust the thermal conditions of their interiors naturally to the human comfort level in 82 % of cases during a year. In such a building, only in 18% of cases during a year, using mechanical systems for cooling the internal spaces is essential. The main problem in this climate is cooling the interior spaces in hot season but in winter these spaces can be kept warm at the level of comfort by using passive or active solar energy or by using simple thermal devices in some situations. This all issues give a good answer to the rules of green architecture which they were carried out by traditional architects as well. Research method of this paper is mainly descriptive and analytical which study the traditional housing of Khorramshahr has been considered for achieving climatic design principles. The results of the studies show that the most problematic issue in this climate is the dry and dusty wind in summer. Since in winter, using solar cooling systems perform a situation that restricts unfavorable climatic factors. In this paper both of above mentioned issues were solved through some guidelines in the area of green architecture. (shrink)

The need for a framework to justify that a model has sufficient credibility to be used as a basis for internal or external (typically regulatory) decision-making is a primary concern when using modelling and simulation (M&S) in healthcare. This chapter reviews published standards on verification, validation, and uncertainty quantification (VVUQ) as well as regulatory guidance that can be used to establish model credibility in this context, providing a potential starting point for a globally harmonised model credibility framework.