895 research outputs found
Resolving conflicting obligations in Mimamsa: a sequent-based approach
No full textThe Philosophical School of Mimamsa provides a treasure trove of more than 2000 years worth of deontic investigations. In this paper we formalize the Mimamsa approach of resolving conflicting obligations by giving preference to the more specific ones. From a technical point of view we provide a method to close a set of prima-facie obligations under a restricted form of monotonicity, using specificity to avoid conflicting obligations in a dyadic non-normal deontic logic. A sequent-based decision procedure for the resulting logic is also provided
Understanding Prescriptive Texts: Rules and Logic as Elaborated by the Mīmāṃsā School
No full textThe Mīmāṃsā school of Indian philosophy elaborated complex ways of interpreting the prescriptive portions of the Vedic sacred
texts. The present article is the result of the collaboration of a group of scholars of logic, computer science, European philosophy and Indian philosophy and aims at the individuation and analysis of the deontic system which is applied but never explicitly discussed in Mīmāṃsā texts. The article outlines the basic distinction between three sorts of principles —hermeneutic, linguistic and deontic. It proposes a mathematical formalization of the deontic principles and uses it to discuss a well-known example of seemingly conflicting statements, namely the prescription to undertake the malefic Śyena sacrifice and the prohibition to perform any harm
Mīmāṃsā Deontic Logic: Proof Theory and Applications
No full textStarting with the deontic principles in Mīmāmsā texts we introduce a new deontic logic. We use general proof-theoretic methods to obtain a cut-free sequent calculus for this logic, resulting in decidability, complexity results and neighbourhood semantics. The latter is used to analyse a well known example of conflicting obligations from the Vedas
Individual Tree Species Classification From Airborne Multisensor Imagery Using Robust PCA
No full textRemote sensing of individual tree species has many applications in resource management, biodiversity assessment, and conservation. Airborne remote sensing using light detection and ranging (LiDAR) and hyperspectral sensors has been used extensively to extract biophysical traits of vegetation and to detect species. However, its application for individual tree mapping remains limited due to the technical challenges of precise coalignment of images acquired from different sensors and accurately delineating individual tree crowns (ITCs). In this study, we developed a generic workflow to map tree species at ITC level from hyperspectral imagery and LiDAR data using a combination of well established and recently developed techniques. The workflow uses a nonparametric image registration approach to coalign images, a multiclass normalized graph cut method for ITC delineation, robust principal component analysis for feature extraction, and support vector machine for species classification. This workflow allows us to automatically map tree species at both pixel- and ITC-level. Experimental tests of the technique were conducted using ground data collected from a fully mapped temperate woodland in the UK. The overall accuracy of pixel-level classification was 91, while that of ITC-level classification was 61. The test results demonstrate the effectiveness of the approach, and in particular the use of robust principal component analysis to prune the hyperspectral dataset and reveal subtle difference among species
Non-smooth Higher-order Optimization on Manifolds
No full textThis thesis introduces a higher-order optimization method for solving non-smooth variational problems on Riemannian manifolds. In this work, we apply the Riemannian Semismooth Newton (RSSN) method to a non-smooth non-linear optimality system derived in recent advances in manifold duality theory. In particular we will show a novel local convergence result for an inexact version of the Riemannian Semismooth Newton method and show state-of-the-art performance in numerical experiments by solving several `2-TV-like problems on manifolds with positive and negative curvature
Discrete and Continuous Models for Partitioning Problems
No full textRecently, variational relaxation techniques for approximating solutions of partitioning problems on continuous image domains have received considerable attention, since they introduce significantly less artifacts than established graph cut-based techniques. This work is concerned with the sources of such artifacts. We discuss the importance of differentiating between artifacts caused by discretization and those caused by relaxation and provide supporting numerical examples. Moreover, we consider in depth the consequences of a recent theoretical result concerning the optimality of solutions obtained using a particular relaxation method. Since the employed regularizer is quite tight, the considered relaxation generally involves a large computational cost. We propose a method to significantly reduce these costs in a fully automatic way for a large class of metrics including tree metrics, thus generalizing a method recently proposed by Strekalovskiy and Cremers (IEEE conference on computer vision and pattern recognition, pp. 1905-1911, 2011). © 2013 Springer Science+Business Media New York.The second and third author were supported by Engineering and Physical Sciences Research Council (EPSRC)-Project EP/H016317/1. This publication is partly based on work supported by Award No. KUK-I1- 007-43, made by King Abdullah University of Science and Technology (KAUST)
Imaging with Kantorovich--Rubinstein Discrepancy
No full text© 2014 Society for Industrial and Applied Mathematics. We propose the use of the Kantorovich-Rubinstein norm from optimal transport in imaging problems. In particular, we discuss a variational regularization model endowed with a Kantorovich- Rubinstein discrepancy term and total variation regularization in the context of image denoising and cartoon-texture decomposition. We point out connections of this approach to several other recently proposed methods such as total generalized variation and norms capturing oscillating patterns. We also show that the respective optimization problem can be turned into a convex-concave saddle point problem with simple constraints and hence can be solved by standard tools. Numerical examples exhibit interesting features and favorable performance for denoising and cartoon-texture decomposition.This research was supported by King Abdullah University of Science and Technology (KAUST) award KUK-I1-007-43 and EPSRC first grant EP/J009539/1, "Sparse & Higher-order Image Restoration."The research of the first author was supported by Leverhulme Early Career Fellowship ECF-2013-436.The research of this author was supported by a Senescyt (Ecuadorian Ministry of Education, Science, and Technology) Prometeo fellowship
Ueber eine Substanz, die einen achtzehngliederigen Ring enthält und dem Gesetz von der Gefrierpunktserniedrigung nicht folgt
No full textn/
Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
No full textThe Craig interpolation property is one of the most fundamental properties of logics. It states that whenever A ⊃ B is valid in a logic, one can find a formula I in the common language of A and B, such that A ⊃ I and I ⊃ B are valid. The formula I is called the interpolant of A ⊃ B. Interpolation was proved for classical first-order logic by Craig and for intuitionistic first-order logic by Schütte.
Lyndon interpolation is a strengthening of the interpolation property in the sense that propositional variables or predicate symbols are only allowed to occur positively (negatively) in the interpolant if they occur positively (negatively) on both sides of the implication. Lyndon interpolation for classical logic has been established by Lyndon.
Little was known about interpolation properties of intermediate logics until Maksimova solved the propositional interpolation problem showing that exactly 7 of these logics have the propositional interpolation property. Her work is based on the algebraic analysis of the logic in question. On first-order level, algebraic semantics are not as well understood and therefore first-order interpolation properties are notoriously hard to determine, even for logics where propositional interpolation is more of less obvious. Hence, it remained an open question which of these 7 logics admit first-order interpolation, among them first-order Gödel logic. Moreover, except of classical and intuitionistic logic, most logics do not seem to admit a Maehara style lemma w.r.t. their established calculi. This applies to e.g. all hypersequent calculi.
In this paper we extend Lyndon interpolation to the prenex ⊃ prenex fragment of Gödel logic using the proof of Lyndon interpolation for propositional Gödel logic from a recent paper of Lellmann and Kuznets. Note that first-order Lyndon interpolation is difficult to establish for first-order logics as most proof-theoretic methods fail
- …
