# zbMATH — the first resource for mathematics

Para-disagreement logics and their implementation through embedding in Coq and SMT. (English) Zbl 1439.03066
Carnielli, Walter (ed.) et al., Contradictions, from consistency to inconsistency. Cham: Springer. Trends Log. Stud. Log. Libr. 47, 139-158 (2018).
Summary: On closer inspection many apparent contradictions turn out to be mere disagreements between distinct sources of information. For example, if a source $$s_1$$ says $$P$$ and a source $$s_2$$ says $$\lnot P$$, their disagreement would only become an actual contradiction if we naively merged what they say into our own knowledge base.
For the entire collection see [Zbl 1419.03004].
##### MSC:
 03B53 Paraconsistent logics 03B35 Mechanization of proofs and logical operations
##### Software:
Archive Formal Proofs; Coq; Gen2sat; GoedelGod; intuit; smt; SMT-LIB; z3
Full Text:
##### References:
 [1] Alchourrón, C.E., P. Gärdenfors, and D. Makinson. 1985. On the logic of theory change: partial meet contraction and revision functions. The Journal of Symbolic Logic 50 (2): 510-530. https://doi.org/10.2307/2274239. · Zbl 0578.03011 [2] Areces, C., and P. Blackburn. 2010. Special issue on hybrid logics. Journal of Applied Logic 8(4): 303-304. https://doi.org/10.1016/j.jal.2010.001. [3] Arieli, O. 2008. Distance-based paraconsistent logics. International Journal of Approximate Reasoning 48(3): 766-783. https://doi.org/10.1016/j.ijar.2007.07.002. · Zbl 1189.03035 [4] Barrett, C., L.M. de Moura, S. Ranise, A. Stump, and C. Tinelli. 2010. The SMT-LIB initiative and the rise of SMT - (HVC 2010 award talk). In: S. Barner, I.G. Harris, D. Kroening, O. Raz (eds.) Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers, Lecture Notes in Computer Science, vol. 6504, p. 3. Springer. https://doi.org/10.1007/978-3-642-19583-9_2. [5] Benzmüller, C., and B. Woltzenlogel Paleo. 2013. Gödel’s god in isabelle/hol. Archive of Formal Proofs 2013. http://afp.sourceforge.net/entries/GoedelGod.shtml. [6] Benzmüller, C., and B. Woltzenlogel Paleo. 2014. Automating Gödel’s ontological proof of god’s existence with higher-order automated theorem provers. In ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014), ed. by T. Schaub, G. Friedrich, B. O’Sullivan Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93-98. IOS Press. https://doi.org/10.3233/978-1-61499-419-0-93. · Zbl 1366.03169 [7] Benzmüller, C., B. Woltzenlogel Paleo. 2014. On logic embeddings and Gödel’s god. In Recent Trends in Algebraic Development Techniques, Theoretical Computer Science and General Issues, ed. by M. Codescu, R. Diaconescu, I. uu, vol. 9463. Springer. https://doi.org/10.1007/978-3-319-28114-8. · Zbl 1327.68013 [8] Benzmüller, C., and B. Woltzenlogel Paleo. 2015. Higher-order modal logics: Automation and applications. In Reasoning Web. Web Logic Rules - 11th International Summer School 2015, Berlin, Germany, July 31 - August 4, 2015, Tutorial Lectures, ed. by W. Faber, A. Paschke, LNCS, vol. 9203, pp. 32-74. Springer. https://doi.org/10.1007/978-3-319-21768-0_2. · Zbl 1358.68273 [9] Benzmüller, C., and B. Woltzenlogel Paleo. 2015. Interacting with modal logics in the Coq proof assistant. In Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings, pp. 398-411. https://doi.org/10.1007/978-3-319-20297-6_25. · Zbl 06496834 [10] Bertossi, L.E. 2011. Database Repairing and Consistent Query Answering. Synthesis Lectures on Data Management. Morgan & Claypool Publishers. https://doi.org/10.2200/S00379ED1V01Y201108DTM020. · Zbl 1238.68004 [11] Bertot, Y., and P. Casteran. 2004. Interactive Theorem Proving and Program Development. Springer. · Zbl 1069.68095 [12] Blackburn, P., M. de Rijke, and Y. Venema. 2001. Modal Logic. New York: Cambridge University Press. · Zbl 0988.03006 [13] Carnielli, W., M.E. Coniglio, and J. Marcos. 2007. Logics of Formal Inconsistency, pp. 1-93. Dordrecht: Springer Netherlands. https://doi.org/10.1007/978-1-4020-6324-4_1. · Zbl 1266.03006 [14] Chomicki, J. 2008. Consistent query answering: The first ten years. In Scalable Uncertainty Management, Second International Conference, SUM 2008, Naples, Italy, October 1-3, 2008. Proceedings, ed. by S. Greco, T. Lukasiewicz, Lecture Notes in Computer Science, vol. 5291, pp. 1-3. Springer. https://doi.org/10.1007/978-3-540-87993-0_1. [15] Claessen, K., and D. Rosén. 2015. SAT modulo intuitionistic implications. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, ed. by M. Davis, A. Fehnker, A. McIver, A. Voronkov, Lecture Notes in Computer Science, vol. 9450, pp. 622-637. Springer. https://doi.org/10.1007/978-3-662-48899-7_43. · Zbl 1435.68363 [16] da Costa, N.C.A., and F.A. Doria. 1995. On jaskowski’s discussive logic. Studia Logica 54(1): 33-60. https://doi.org/10.1007/BF01058531. · Zbl 0818.03012 [17] de Moura, L.M., and N. Bjørner. 2008. Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, ed. by C.R. Ramakrishnan, J. Rehof, Lecture Notes in Computer Science, vol. 4963, pp. 337-340. Springer. https://doi.org/10.1007/978-3-540-78800-3_24. [18] Lenzerini, M. 2002. Data integration: A theoretical perspective. In Proceedings of the Twenty-first ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 3-5, Madison, Wisconsin, USA, ed. by L. Popa, S. Abiteboul, P.G. Kolaitis, pp. 233-246. ACM. https://doi.org/10.1145/543613.543644. [19] Marcos, J. 2005. Modality and paraconsistency. The Logica Yearbook 2004: 213-222. [20] Paulin-Mohring, C. 2015. Introduction to the calculus of inductive constructions. In All about Proofs, Proofs for All, Mathematical Logic and Foundations, ed. by D. Delahaye, B. Woltzenlogel Paleo. London: College Publications. · Zbl 1431.03026 [21] Staworko, S., J. Chomicki, and J. Marcinkowski. 2012. Prioritized repairing and consistent query answering in relational databases. Annals of Mathematics and Artificial Intelligence 64(2-3): 209-246. https://doi.org/10.1007/s10472-012-9288-8. · Zbl 1250.68099 [22] Zohar, Y., and A. Zamansky. 2016. Gen2sat: An automated tool for deciding derivability in analytic pure sequent calculi. In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, ed. by N. Olivetti, A. Tiwari, Lecture Notes in Computer Science, vol. 9706, pp. 487-495. Springer. https://doi.org/10.1007/978-3-319-40229-1_33. · Zbl 06623281 [23] Zwicker, W.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.