All Normal Extensions of S5-squared Are Finitely Axiomatizable

We prove that every normal extension of the bi-modal system S5² is finitely axiomatizable and that every proper normal extension has NP-complete satisfiability problem.Presented by Heinrich Wansing     

Student Evaluations and Moral Hazard

Most universities solicit feedback from students at the end of a course in order to assess student perceptions of the course. This feedback is used for various objectives, including for evaluating teaching by academic administrators. One would therefore expect faculty to rationally take this into account while formulating their teaching strategy. In certain cases, such strategic considerations can give rise to moral hazard. I have modelled the situation using the well-known Prisoners Dilemma game and found that in equilibrium, the teaching style will be examination-centric, while considerations of societal good would demand that the teaching style be knowledge-centric. I also discuss the policy implications for this finding.     

On teaching computer ethics within a computer science department

The author has surveyed a quarter of the accredited undergraduate computer science programs in the United States. More than half of these programs offer a “social and ethical implications of computing” course taught by a computer science faculty member, and there appears to be a trend toward teaching ethics classes within computer science departments. Although the decision to create an “in house” computer ethics course may sometimes be a pragmatic response to pressure from the accreditation agency, this paper argues that teaching ethics within a computer science department can provide students and faculty members with numerous benefits. The paper lists topics that can be covered in a computer ethics course and offers some practical suggestions for making the course successful. An earlier version of this paper was presented at the 2005 conference, Ethics and Social Responsibility in Engineering and Technology, Linking Workplace Ethics and Education, co-hosted by Gonzaga University and Loyola Marymount University, Los Angeles, California, 9–10 June 2005.     

TPS: A hybrid automatic-interactive system for developing proofs

The theorem proving system Tps provides support for constructing proofs using a mix of automation and user interaction, and for manipulating and inspecting proofs. Its library facilities allow the user to store and organize work. Mathematical theorems can be expressed very naturally in Tps using higher-order logic. A number of proof representations are available in Tps, so proofs can be inspected from various perspectives.     

Analysis of proctor marking accuracy in a computer-aided personalized system of instruction course

In a computer-aided version of Keller's personalized system of instruction (CAPSI), students within a course were assigned by a computer to be proctors for tests. Archived data from a CAPSI-taught behavior modification course were analyzed to assess proctor accuracy in marking answers as correct or incorrect. Overall accuracy was increased by having each test marked independently by two proctors, and was higher on incorrect answers when the degree of incorrectness was larger.     

Standard Quantification Theory in the Analysis of English

Standard first-order logic plus quantifiers of all finite orders (SFOL) faces four well-known difficulties when used to characterize the behavior of certain English quantifier phrases. All four difficulties seem to stem from the typed structure of SFOL models. The typed structure of SFOL models is in turn a product of an asymmetry between the meaning of names and the meaning of predicates, the element-set asymmetry. In this paper we examine a class of models in which this asymmetry of meaning is removed. The models of this class permit definitions of the quantifiers which allow a desirable flexibility in fixing the domain of quantification. Certain SFOL type restrictions are thereby avoided. The resulting models of English validate all of the standard first-order logical truths and are free of the four deficiencies of SFOL models.     

Quantum Logic as a Fragment of Independence-Friendly Logic

The working assumption of this paper is that noncommuting variables are irreducibly interdependent. The logic of such dependence relations is the author's independence-friendly (IF) logic, extended by adding to it sentence-initial contradictory negation ¬ over and above the dual (strong) negation . Then in a Hilbert space turns out to express orthocomplementation. This can be extended to any logical space, which makes it possible to define the dimension of a logical space. The received Birkhoff and von Neumann quantum logic can be interpreted by taking their disjunction to be ¬(A & B). Their logic can thus be mapped into a Boolean structure to which an additional operator has been added.     

Quantum Logic in Intuitionistic Perspective

In their seminal paper Birkhoff and von Neumann revealed the following dilemma:[ ] whereas for logicians the orthocomplementation properties of negation were the ones least able to withstand a critical analysis, the study of mechanics points to the distributive identities as the weakest link in the algebra of logic.In this paper we eliminate this dilemma, providing a way for maintaining both. Via the introduction of the "missing" disjunctions in the lattice of properties of a physical system while inheriting the meet as a conjunction we obtain a complete Heyting algebra of propositions on physical properties. In particular there is a bijective correspondence between property lattices and propositional lattices equipped with a so called operational resolution, an operation that exposes the properties on the level of the propositions. If the property lattice goes equipped with an orthocomplementation, then this bijective correspondence can be refined to one with propositional lattices equipped with an operational complementation, as such establishing the claim made above. Formally one rediscovers via physical and logical considerations as such respectively a specification and a refinement of the purely mathematical result by Bruns and Lakser (1970) on injective hulls of meet-semilattices. From our representation we can derive a truly intuitionistic functional implication on property lattices, as such confronting claims made in previous writings on the matter. We also make a detailed analysis of disjunctivity vs. distributivity and finitary vs. infinitary conjunctivity, we briefly review the Bruns-Lakser construction and indicate some questions which are left open.