Normative conditional reasoning as a fragment of HOL

要約

規範的（好みに基づく）条件付き推論の機械化に関するいくつかの結果を報告します。
私たちは、条件付き義務のための Aqvist のシステム E (およびその拡張) に焦点を当てています。
私たちの機械化は、Isabelle/HOL への浅い意味の埋め込みによって実現されます。
このフレームワークの 2 つの用途を考えます。
1 つ目は、検討中のロジックについてメタ推論するためのツールとしてです。
私たちはこれを、モーダル ロジック キューブで以前に達成されたものと同様に、義務的対応 (広義に考えられている) および関連事項の自動検証に使用します。
2 番目の用途は、倫理的議論を評価するためのツールとしてです。
私たちは、人口倫理におけるよく知られたパラドックス、パーフィットの不快な結論をコンピュータでエンコードしたものを提供します。
提示されたコード化が、不快な結論の魅力と説得力を増加させるか減少させるかは、私たちが哲学と倫理に委ねたい問題です。

要約(オリジナル)

We report some results regarding the mechanization of normative (preference-based) conditional reasoning. Our focus is on Aqvist’s system E for conditional obligation (and its extensions). Our mechanization is achieved via a shallow semantical embedding in Isabelle/HOL. We consider two possible uses of the framework. The first one is as a tool for meta-reasoning about the considered logic. We employ it for the automated verification of deontic correspondences (broadly conceived) and related matters, analogous to what has been previously achieved for the modal logic cube. The second use is as a tool for assessing ethical arguments. We provide a computer encoding of a well-known paradox in population ethics, Parfit’s repugnant conclusion. Whether the presented encoding increases or decreases the attractiveness and persuasiveness of the repugnant conclusion is a question we would like to pass on to philosophy and ethics.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google