This series provides a forum for cutting-edge studies in logic and the modern philosophy of language as well as for publications in the field of analytical metaphysics.
It is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system Fat, a predicative calculus with only two connectives: ...the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of the intuitionistic propositional logic in which commuting conversions are not needed.
We show that there is a purely proof-theoretic proof of the Rasiowa-Harrop disjunction property for the full intuitionistic propositional calculus (IPC), via natural deduction, in which commuting ...conversions are not needed. Such proof is based on a sound and faithful embedding of IPC into an atomic polymorphic system. This result strengthens a homologous result for the disjunction property of IPC (presented in a recent paper co-authored with Fernando Ferreira) and answers a question then posed by Pierluigi Minari.
In their Unifying Theories of Programming (UTP), Hoare & He use the alphabetised relational calculus to give denotational semantics to a wide variety of constructs taken from different programming ...paradigms. In this chapter, we give a tutorial introduction to the semantics of CSP processes, as presented in Chapter 3. We start with a summarised introduction of the alphabetised relational calculus and the theory of designs, which are pre-post specifications in the style of specification statements. Afterwards, we present in detail a theory for reactive processes. Later, we combine the theories of designs and reactive processes to provide the model for CSP processes. Finally, we compare this new model with the standard failures-divergences model for CSP.
Much effort has been made to build appropriate models for a boost converter. However, these models were described as inexact or complicated expressions in both continuous conduction mode (CCM) and ...discontinuous conduction mode (DCM). This study proposes a new modelling method based on propositional calculus and linear constraint. First, the equivalent operating conditions (OCs) of the boost converter in CCM and DCM are formulated. Second, according to the equivalent translation principle, the OCs of the boost converter in three different modes can be transformed into two linear inequalities. Moreover then, a unified model of the boost converter in CCM and DCM is obtained. Compared with mixed logical dynamical model, the proposed model (PM) of the boost converter is more concise. In addition, the PM is a large-signal model in the theoretical analysis. Finally, the model is simulated in MATLAB under different load conditions and its effectiveness is well verified by simulation results. Moreover, the experimental results are consistent with the simulation results.
PDF
