A Calculus of Substitutions for DPL

We consider substitutions in order sensitive situations, having in the back of our minds the case of dynamic predicate logic (DPL) with a stack semantics. We start from the semantic intuition that substitutions are move instructions on stacks: the syntactic operation [y/x] is matched by the instruction to move the value of the y-stack to the x-stack. We can describe these actions in the positive fragment of DPLE. Hence this fragment counts as a logic for DPL-substitutions. We give a calculus for the fragment and prove soundness and completeness.     

盆腔炎性疾病的预防

盆腔炎性疾病（pelvic inflammatory disease,PID）是影响妇女健康的常见病,针对其发病的诱因,预防PID可以从以下几个方面进行：（1）加强性教育,减少性传播疾病;（2）积极做好妇女的卫生保健指导工作;（3）重视筛查、早期诊断及一次性根治下生殖道感染;（4）提高医务人员的理论水平和技术,避免医源性感染;（5）持续正确选择避孕措施;（6）避免阴道冲洗。此外,长期放置宫内节育器不会增加PID的风险;口服避孕药对PID无明显预防作用,而仅仅与减轻其严重症状有关。     

Program Extraction from Normalization Proofs

This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.     

FOIL Axiomatized

In an earlier paper, [5], I gave semantics and tableau rules for a simple firstorder intensional logic called FOIL, in which both objects and intensions are explicitly present and can be quantified over. Intensions, being non-rigid, are represented in FOIL as (partial) functions from states to objects. Scoping machinery, predicate abstraction, is present to disambiguate sentences like that asserting the necessary identity of the morning and the evening star, which is true in one sense and not true in another.In this paper I address the problem of axiomatizing FOIL. I begin with an interesting sublogic with predicate abstraction and equality but no quantifiers. In [2] this sublogic was shown to be undecidable if the underlying modal logic was at least K4, though it is decidable in other cases. The axiomatization given is shown to be complete for standard logics without a symmetry condition. The general situation is not known. After this an axiomatization for the full FOIL is given, which is straightforward after one makes a change in the point of view.This paper is a version of the invited talk given by the author at the conference Trends in Logic III, dedicated to the memory of A. MOSTOWSKI, H. RASIOWA and C. RAUSZER, and held in Warsaw and Ruciane-Nida from 23rd to 25th September 2005.     

缺位与越位的思考——医疗保健体制改革的定位

政府的缺位和医院的越位是目前医疗体制改革的症结所在。政府将医院推向市场,意味着政府放弃医疗的社会保障职能。医院失去政府的约束和支持,逐利将成为其必然行为。平价医院只是缓和矛盾的一时之计,只要医院不退出市场,看病难、看病贵就难有灵丹妙药,医患关系也将难以和谐。