Reasoning Tools for Deontic logic and Applications to Indian Sacred Texts

As one of the fundamental systems of Indian philosophy, the Mimamsa school has had a profound impact on Indian philosophy, theology and law. Focusing on the interpretation of the prescriptive parts of the Indian Sacred Texts (the Vedas), Mimamsa scholars over more than two millennia developed an extensive theory about deontic concepts such as ''obligation'' and ''prohibition''. Yet, despite its clear significance, and despite the structure of the texts lending themselves to rigorous analysis, no formal study of Mimamsa reasoning has been undertaken so far and most of its specificities have remained unexplored or misunderstood. We aim to fill this gap and provide a better understanding of the Mimamsa texts via a formal analysis based on deontic logics. The latter are logical systems apt to reason about norms, and hence well suited to formalizing the many different aspects of Mimamsa deontic reasoning. Our investigation requires the availability of reasoning tools for these logics (analytic calculi, useful semantics, complexity results and theorem provers), whose construction and study is currently logic-tailored. We aim to introduce such tools for deontic logics in a uniform and systematic way, with particular emphasis on general methods for the construction of analytic calculi from Hilbert-style axioms. Our tools are expected to be useful in various areas, but within the project they will be used for analyzing and understanding the rationale behind the Mimamsa interpretation of the Vedas.