- Submit
-
Browse
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- More
Switch to: Citations
References in:
Add references
You must login to add references.
|
|
|
We translate unconstrained and constrained input/output logics as introduced by Makinson and van der Torre to modal logics, using adaptive logics for the constrained case. The resulting reformulation has some additional benefits. First, we obtain a proof-theoretic characterization of input/output logics. Second, we demonstrate that our framework naturally gives rise to useful variants and allows to express important notions that go beyond the expressive means of input/output logics, such as violations and sanctions. |
|
|
|
|
|
|
|
|
Formal arguments are often represented by pairs, but in this paper we consider normative arguments represented by sequences of triples, where constitutive norms derive institutional facts from brute facts, and regulative norms derive deontic facts like obligations and permissions from institutional facts. The institutional facts may be seen as the reasons explaining or warranting the deontic obligations and permissions, and therefore they can be attacked by other normative arguments too. We represent different aspects of normative reasoning by different kinds of (...) |
|
|
We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory. |
|
|
The implementation of moral decision making abilities in artificial intelligence (AI) is a natural and necessary extension to the social mechanisms of autonomous software agents and robots. Engineers exploring design strategies for systems sensitive to moral considerations in their choices and actions will need to determine what role ethical theory should play in defining control architectures for such systems. The architectures for morally intelligent agents fall within two broad approaches: the top-down imposition of ethical theories, and the bottom-up building of (...) |
|
|
Computational philosophy is the use of mechanized computational techniques to unearth philosophical insights that are either difficult or impossible to find using traditional philosophical methods. Computational metaphysics is computational philosophy with a focus on metaphysics. In this paper, we (a) develop results in modal metaphysics whose discovery was computer assisted, and (b) conclude that these results work not only to the obvious benefit of philosophy but also, less obviously, to the benefit of computer science, since the new computational techniques that (...) |
|
|
Robot ethics encompasses ethical questions about how humans should design, deploy, and treat robots; machine morality encompasses questions about what moral capacities a robot should have and how these capacities could be computationally implemented. Publications on both of these topics have doubled twice in the past 10 years but have often remained separate from one another. In an attempt to better integrate the two, I offer a framework for what a morally competent robot would look like and discuss a number (...) |
|
|
|
|
|
In a range of contexts, one comes across processes resembling inference, but where input propositions are not in general included among outputs, and the operation is not in any way reversible. Examples arise in contexts of conditional obligations, goals, ideals, preferences, actions, and beliefs. Our purpose is to develop a theory of such input/output operations. Four are singled out: simple-minded, basic (making intelligent use of disjunctive inputs), simple-minded reusable (in which outputs may be recycled as inputs), and basic reusable. They (...) |
|
|
|
|
|
|
|
|
|
|
|
I present a variant of with time, called, interpreted in standard Kripke semantics. On the syntactic level, is nothing but the extension of atemporal individual by: the future tense and past tense operators, and the operator of group agency for the grand coalition. A sound and complete axiomatisation for is given. Moreover, it is shown that supports reasoning about interesting normative concepts such as the concepts of achievement obligation and commitment. |
|
|
|
|
|
This paper tackles an open problem posed by Åqvist. It is the problem of whether his dyadic deontic systemsEandFare complete with respect to their intended Hanssonian preference-based semantics. It is known that there are two different ways of interpreting what it means for a world to be best or top-ranked among alternatives. This can be understood as saying that it is optimal among them, or maximal among them. First, it is established that, under either the maximality rule or the optimality (...) |
|
|
This paper reports completeness results for dyadic deontic logics in the tradition of Hansson’s systems. There are two ways to understand the core notion of best antecedent-worlds, which underpins such systems. One is in terms of maximality, and the other in terms of optimality. Depending on the choice being made, one gets different evaluation rules for the deontic modalities, but also different versions of the so-called limit assumption. Four of them are disentangled, and compared. The main observation of this paper (...) |
|
|
|
|
|
|
|
|
|
|
|
In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-order calculi with respect to these model classes. |
|
|
|
|
|
A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion. |
|
|
In a range of contexts, one comes across processes resembling inference, but where input propositions are not in general included among outputs, and the operation is not in any way reversible. Examples arise in contexts of conditional obligations, goals, ideals, preferences, actions, and beliefs. Our purpose is to develop a theory of such input/output operations. Four are singled out: simple-minded, basic (making intelligent use of disjunctive inputs), simple-minded reusable (in which outputs may be recycled as inputs), and basic reusable. They (...) |
|
|
|
|
|
Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API (...) |
|
|
|
|
|
An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has been proposed as a potential means to bound the impact of artificial general intelligence. |
|
|
We show that Carmo and Jones’ condition 5 conflicts with the other conditions on their models for contrary-to-duty obligations. We then propose a resolution to the conflict. |
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-9b866bbb8-sfvjl uwo