Vasileiou, Stylianos Loukas; Yeoh, William; Son, Tran Cao; Kumar, Ashwin; Cashmore, Michael; Magazzeni, Dianele A logic-based explanation generation framework for classical and hybrid planning problems. (English) Zbl 07527556 J. Artif. Intell. Res. (JAIR) 73, 1473-1534 (2022). MSC: 68Txx PDF BibTeX XML Cite \textit{S. L. Vasileiou} et al., J. Artif. Intell. Res. (JAIR) 73, 1473--1534 (2022; Zbl 07527556) Full Text: DOI OpenURL
Belardinelli, Francesco; Lomuscio, Alessio; Malvone, Vadim; Yu, Emily Approximating perfect recall when model checking strategic abilities: theory and applications. (English) Zbl 07527543 J. Artif. Intell. Res. (JAIR) 73, 897-932 (2022). MSC: 68Txx PDF BibTeX XML Cite \textit{F. Belardinelli} et al., J. Artif. Intell. Res. (JAIR) 73, 897--932 (2022; Zbl 07527543) Full Text: DOI OpenURL
Toro Icarte, Rodrigo; Klassen, Toryn Q.; Valenzano, Richard; McIlraith, Sheila A. Reward machines: exploiting reward function structure in reinforcement learning. (English) Zbl 07470384 J. Artif. Intell. Res. (JAIR) 73, 173-208 (2022). MSC: 68Txx PDF BibTeX XML Cite \textit{R. Toro Icarte} et al., J. Artif. Intell. Res. (JAIR) 73, 173--208 (2022; Zbl 07470384) Full Text: DOI arXiv OpenURL
De Giacomo, Giuseppe; Felli, Paolo; Logan, Brian; Patrizi, Fabio; Sardiña, Sebastian Situation calculus for controller synthesis in manufacturing systems with first-order state representation. (English) Zbl 1481.93036 Artif. Intell. 302, Article ID 103598, 30 p. (2022). MSC: 93B50 90B30 93-04 90-04 PDF BibTeX XML Cite \textit{G. De Giacomo} et al., Artif. Intell. 302, Article ID 103598, 30 p. (2022; Zbl 1481.93036) Full Text: DOI OpenURL
Castillo, Oscar; Rodriguez, Luis A new meta-heuristic optimization algorithm based on the string theory paradigm from physics. (English) Zbl 1482.68002 SpringerBriefs in Applied Sciences and Technology. Computational Intelligence. Cham: Springer (ISBN 978-3-030-82287-3/pbk; 978-3-030-82288-0/ebook). viii, 71 p. (2022). MSC: 68-02 90-02 68T20 68T37 81T30 90C59 93C42 93C85 PDF BibTeX XML Cite \textit{O. Castillo} and \textit{L. Rodriguez}, A new meta-heuristic optimization algorithm based on the string theory paradigm from physics. Cham: Springer (2022; Zbl 1482.68002) Full Text: DOI OpenURL
Fuenmayor, David; Steen, Alexander A flexible approach to argumentation framework analysis using theorem proving. (English) Zbl 1484.68228 Liao, Beishui (ed.) et al., Logics for new-generation AI 2021. First international workshop, LNGAI 2021, June, 18–20 2021, Hangzhou, China. London: College Publications. 18-32 (2021). MSC: 68T27 68V15 PDF BibTeX XML Cite \textit{D. Fuenmayor} and \textit{A. Steen}, in: Logics for new-generation AI 2021. First international workshop, LNGAI 2021, June, 18--20 2021, Hangzhou, China. London: College Publications. 18--32 (2021; Zbl 1484.68228) OpenURL
Darwiche, Adnan; Marquis, Pierre On quantifying literals in Boolean logic and its applications to explainable AI. (English) Zbl 07470355 J. Artif. Intell. Res. (JAIR) 72, 285-328 (2021). MSC: 68Txx PDF BibTeX XML Cite \textit{A. Darwiche} and \textit{P. Marquis}, J. Artif. Intell. Res. (JAIR) 72, 285--328 (2021; Zbl 07470355) Full Text: DOI arXiv OpenURL
Claessen, Koen; Lillieström, Ann Handling transitive relations in first-order automated reasoning. (English) Zbl 07461266 J. Autom. Reasoning 65, No. 8, 1097-1124 (2021). MSC: 68V15 PDF BibTeX XML Cite \textit{K. Claessen} and \textit{A. Lillieström}, J. Autom. Reasoning 65, No. 8, 1097--1124 (2021; Zbl 07461266) Full Text: DOI OpenURL
Rabe, Markus N.; Szegedy, Christian Towards the automatic mathematician. (English) Zbl 07437070 Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 25-37 (2021). MSC: 03B35 68V15 PDF BibTeX XML Cite \textit{M. N. Rabe} and \textit{C. Szegedy}, Lect. Notes Comput. Sci. 12699, 25--37 (2021; Zbl 07437070) Full Text: DOI OpenURL
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare Towards satisfiability modulo parametric bit-vectors. (English) Zbl 07433026 J. Autom. Reasoning 65, No. 7, 1001-1025 (2021). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Niemetz} et al., J. Autom. Reasoning 65, No. 7, 1001--1025 (2021; Zbl 07433026) Full Text: DOI OpenURL
Steen, Alexander; Benzmüller, Christoph Extensional higher-order paramodulation in Leo-III. (English) Zbl 07432187 J. Autom. Reasoning 65, No. 6, 775-807 (2021). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Steen} and \textit{C. Benzmüller}, J. Autom. Reasoning 65, No. 6, 775--807 (2021; Zbl 07432187) Full Text: DOI arXiv OpenURL
Hou, Zhe Fundamentals of logic and computation. With practical automated reasoning and verification. (English) Zbl 07420661 Texts in Computer Science. Cham: Springer (ISBN 978-3-030-87881-8/hbk; 978-3-030-87882-5/ebook). x, 221 p. (2021). Reviewer: Marco Benini (Como) MSC: 68-01 03-01 68Q60 68V20 PDF BibTeX XML Cite \textit{Z. Hou}, Fundamentals of logic and computation. With practical automated reasoning and verification. Cham: Springer (2021; Zbl 07420661) Full Text: DOI OpenURL
Tena Cucala, David; Cuenca Grau, Bernardo; Horrocks, Ian Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \). (English) Zbl 07418675 Artif. Intell. 298, Article ID 103518, 66 p. (2021). MSC: 68Txx PDF BibTeX XML Cite \textit{D. Tena Cucala} et al., Artif. Intell. 298, Article ID 103518, 66 p. (2021; Zbl 07418675) Full Text: DOI OpenURL
Peitl, Tomáš; Szeider, Stefan Finding the hardest formulas for resolution. (English) Zbl 07406494 J. Artif. Intell. Res. (JAIR) 72, 69-97 (2021). MSC: 68Txx PDF BibTeX XML Cite \textit{T. Peitl} and \textit{S. Szeider}, J. Artif. Intell. Res. (JAIR) 72, 69--97 (2021; Zbl 07406494) Full Text: DOI OpenURL
Affeldt, Reynald; Garrigue, Jacques; Nowak, David; Saikawa, Takafumi A trustful monad for axiomatic reasoning with probability and nondeterminism. (English) Zbl 07400737 J. Funct. Program. 31, Paper No. e17, 38 p. (2021). Reviewer: Alexandre Goy (Lyon) MSC: 03B70 68N18 68V15 PDF BibTeX XML Cite \textit{R. Affeldt} et al., J. Funct. Program. 31, Paper No. e17, 38 p. (2021; Zbl 07400737) Full Text: DOI arXiv OpenURL
Lyaletski, A. V. Evidence algorithm and sad systems: past and possible future. (English) Zbl 07378038 Cybern. Syst. Anal. 57, No. 1, 9-15 (2021) and Kibern. Sist. Anal. 57, No. 1, 12-20 (2021). MSC: 68Txx 68Qxx 68-XX PDF BibTeX XML Cite \textit{A. V. Lyaletski}, Cybern. Syst. Anal. 57, No. 1, 9--15 (2021; Zbl 07378038) Full Text: DOI OpenURL
Chan, Hing Lun; Norrish, Michael Mechanisation of the AKS algorithm. (English) Zbl 1465.68301 J. Autom. Reasoning 65, No. 2, 205-256 (2021). MSC: 68V20 03B35 11A51 11Y11 11Y16 68Q25 PDF BibTeX XML Cite \textit{H. L. Chan} and \textit{M. Norrish}, J. Autom. Reasoning 65, No. 2, 205--256 (2021; Zbl 1465.68301) Full Text: DOI OpenURL
Cantone, Domenico; Nicolosi-Asmundo, Marianna; Santamaria, Daniele Francesco An improved set-based reasoner for the description logic \(\mathcal{DL}_\mathrm{D}^{4,\times\dagger}\). (English) Zbl 07355381 Fundam. Inform. 178, No. 4, 315-346 (2021). MSC: 68-XX PDF BibTeX XML Cite \textit{D. Cantone} et al., Fundam. Inform. 178, No. 4, 315--346 (2021; Zbl 07355381) Full Text: DOI OpenURL
Drămnesc, Isabela; Jebelean, Tudor Synthesis of sorting algorithms using multisets in Theorema. (English) Zbl 1455.68245 J. Log. Algebr. Methods Program. 119, Article ID 100635, 26 p. (2021). MSC: 68V15 68P10 PDF BibTeX XML Cite \textit{I. Drămnesc} and \textit{T. Jebelean}, J. Log. Algebr. Methods Program. 119, Article ID 100635, 26 p. (2021; Zbl 1455.68245) Full Text: DOI arXiv OpenURL
Gaggl, Sarah Alice; Rudolph, Sebastian; Straß, Hannes On the decomposition of abstract dialectical frameworks and the complexity of naive-based semantics. (English) Zbl 1476.68251 J. Artif. Intell. Res. (JAIR) 70, 1-64 (2021). MSC: 68T27 68Q25 PDF BibTeX XML Cite \textit{S. A. Gaggl} et al., J. Artif. Intell. Res. (JAIR) 70, 1--64 (2021; Zbl 1476.68251) Full Text: DOI OpenURL
Abzianidze, Lasha Solving textual entailment with the theorem prover for natural language. (English) Zbl 1476.68297 Appl. Math. Inform. Mech. 25, No. 2, 114-136 (2020). MSC: 68V15 03B65 68T50 PDF BibTeX XML Cite \textit{L. Abzianidze}, Appl. Math. Inform. Mech. 25, No. 2, 114--136 (2020; Zbl 1476.68297) Full Text: Link OpenURL
Kučera, Petr; Savický, Petr Bounds on the size of PC and URC formulas. (English) Zbl 07299924 J. Artif. Intell. Res. (JAIR) 69, 1395-1420 (2020). MSC: 68Txx PDF BibTeX XML Cite \textit{P. Kučera} and \textit{P. Savický}, J. Artif. Intell. Res. (JAIR) 69, 1395--1420 (2020; Zbl 07299924) Full Text: DOI arXiv OpenURL
Miranda-Perea, Favio E.; González Huesca, Lourdes del Carmen; Linares-Arévalo, P. Selene Interactive proof-search for equational reasoning. (English) Zbl 1477.03033 Log. J. IGPL 28, No. 6, 1155-1181 (2020). MSC: 03B35 68V15 08B05 PDF BibTeX XML Cite \textit{F. E. Miranda-Perea} et al., Log. J. IGPL 28, No. 6, 1155--1181 (2020; Zbl 1477.03033) Full Text: DOI OpenURL
Del Vescovo, Chiara; Horridge, Matthew; Parsia, Bijan; Sattler, Uli; Schneider, Thomas; Zhao, Haoruo Modular structures and atomic decomposition in ontologies. (English) Zbl 07283370 J. Artif. Intell. Res. (JAIR) 69, 963-1021 (2020). MSC: 68Txx PDF BibTeX XML Cite \textit{C. Del Vescovo} et al., J. Artif. Intell. Res. (JAIR) 69, 963--1021 (2020; Zbl 07283370) Full Text: DOI OpenURL
Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. (English) Zbl 07274579 Artif. Intell. 287, Article ID 103348, 28 p. (2020). MSC: 68Txx PDF BibTeX XML Cite \textit{C. Benzmüller} et al., Artif. Intell. 287, Article ID 103348, 28 p. (2020; Zbl 07274579) Full Text: DOI arXiv OpenURL
Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier First-order automated reasoning with theories: when deduction modulo theory meets practice. (English) Zbl 1468.68282 J. Autom. Reasoning 64, No. 6, 1001-1050 (2020). MSC: 68V15 03B35 PDF BibTeX XML Cite \textit{G. Burel} et al., J. Autom. Reasoning 64, No. 6, 1001--1050 (2020; Zbl 1468.68282) Full Text: DOI HAL OpenURL
Syeda, Hira Taqdees; Klein, Gerwin Formal reasoning under cached address translation. (English) Zbl 1468.68070 J. Autom. Reasoning 64, No. 5, 911-945 (2020). MSC: 68N25 03B70 68N30 68V15 PDF BibTeX XML Cite \textit{H. T. Syeda} and \textit{G. Klein}, J. Autom. Reasoning 64, No. 5, 911--945 (2020; Zbl 1468.68070) Full Text: DOI OpenURL
Benzmüller, Christoph; Fuenmayor, David Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument. (English) Zbl 1461.03021 Bull. Sect. Log., Univ. Łódź, Dep. Log. 49, No. 2, 127-148 (2020). MSC: 03B45 03B35 03-08 PDF BibTeX XML Cite \textit{C. Benzmüller} and \textit{D. Fuenmayor}, Bull. Sect. Log., Univ. Łódź, Dep. Log. 49, No. 2, 127--148 (2020; Zbl 1461.03021) Full Text: DOI arXiv OpenURL
Kirchner, Daniel; Benzmüller, Christoph; Zalta, Edward N. Mechanizing Principia logico-metaphysica in functional type-theory. (English) Zbl 1484.03020 Rev. Symb. Log. 13, No. 1, 206-218 (2020). MSC: 03B35 03A05 03B38 03B45 68V15 PDF BibTeX XML Cite \textit{D. Kirchner} et al., Rev. Symb. Log. 13, No. 1, 206--218 (2020; Zbl 1484.03020) Full Text: DOI arXiv OpenURL
Baumgartner, Peter; Schmidt, Renate A. Blocking and other enhancements for bottom-up model generation methods. (English) Zbl 1468.68279 J. Autom. Reasoning 64, No. 2, 197-251 (2020). MSC: 68V15 03B35 03B70 PDF BibTeX XML Cite \textit{P. Baumgartner} and \textit{R. A. Schmidt}, J. Autom. Reasoning 64, No. 2, 197--251 (2020; Zbl 1468.68279) Full Text: DOI OpenURL
Kovács, Zoltán; Recio, Tomás; Vélez, M. Pilar Reasoning about linkages with dynamic geometry. (English) Zbl 1440.68341 J. Symb. Comput. 97, 16-30 (2020). Reviewer: Nelly Villamizar (Swansea) MSC: 68W30 51M15 68U05 68V15 70B15 PDF BibTeX XML Cite \textit{Z. Kovács} et al., J. Symb. Comput. 97, 16--30 (2020; Zbl 1440.68341) Full Text: DOI OpenURL
Dimopoulos, Yannis; Gebser, Martin; Lühne, Patrick; Romero, Javier; Schaub, Torsten plasp 3: towards effective ASP planning. (English) Zbl 1472.68182 Theory Pract. Log. Program. 19, No. 3, 477-504 (2019). MSC: 68T20 68N17 68T30 PDF BibTeX XML Cite \textit{Y. Dimopoulos} et al., Theory Pract. Log. Program. 19, No. 3, 477--504 (2019; Zbl 1472.68182) Full Text: DOI OpenURL
Hanna, Gila (ed.); Reid, David A. (ed.); De Villiers, Michael (ed.) Proof technology in mathematics research and teaching. (English) Zbl 1451.97008 Mathematics Education in the Digital Era 14. Cham: Springer (ISBN 978-3-030-28482-4/hbk; 978-3-030-28485-5/pbk; 978-3-030-28483-1/ebook). viii, 379 p. (2019). MSC: 97-06 97U50 97E50 68V15 00B15 PDF BibTeX XML Cite \textit{G. Hanna} (ed.) et al., Proof technology in mathematics research and teaching. Cham: Springer (2019; Zbl 1451.97008) Full Text: DOI Link OpenURL
Huang, Pei; Liu, Minghao; Ge, Cunjing; Ma, Feifei; Zhang, Jian Investigating the existence of orthogonal golf designs via satisfiability testing. (English) Zbl 1467.81076 Bradford, Russell (ed.), Proceedings of the 44th international symposium on symbolic and algebraic computation, ISSAC ’19, Beijing, China, July 15–18, 2019. New York, NY: Association for Computing Machinery (ACM). 203-210 (2019). MSC: 81T20 68V15 05B15 PDF BibTeX XML Cite \textit{P. Huang} et al., in: Proceedings of the 44th international symposium on symbolic and algebraic computation, ISSAC '19, Beijing, China, July 15--18, 2019. New York, NY: Association for Computing Machinery (ACM). 203--210 (2019; Zbl 1467.81076) Full Text: DOI OpenURL
Fuenmayor, David; Benzmüller, Christoph Computational hermeneutics: an integrated approach for the logical analysis of natural-language arguments. (English) Zbl 07229671 Liao, Beishui (ed.) et al., Dynamics, uncertainty and reasoning. Selected papers of the second Chinese conference on logic and argumentation (CLAR 2018), Hangzhou, China, June 16–17, 2018. Singapore: Springer. Log. Asia: Stud. Log. Libr., 187-207 (2019). MSC: 68V15 68T50 PDF BibTeX XML Cite \textit{D. Fuenmayor} and \textit{C. Benzmüller}, in: Dynamics, uncertainty and reasoning. Selected papers of the second Chinese conference on logic and argumentation (CLAR 2018), Hangzhou, China, June 16--17, 2018. Singapore: Springer. 187--207 (2019; Zbl 07229671) Full Text: DOI OpenURL
Tena Cucala, David; Cuenca Grau, Bernardo; Horrocks, Ian 15 years of consequence-based reasoning. (English) Zbl 1444.68192 Lutz, Carsten (ed.) et al., Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 11560, 573-587 (2019). MSC: 68T27 68T30 68V15 PDF BibTeX XML Cite \textit{D. Tena Cucala} et al., Lect. Notes Comput. Sci. 11560, 573--587 (2019; Zbl 1444.68192) Full Text: DOI OpenURL
Britz, Katarina; Varzinczak, Ivan Preferential tableaux for contextual defeasible \(\mathcal{ALC}\). (English) Zbl 1435.68312 Cerrito, Serenella (ed.) et al., Automated reasoning with analytic tableaux and related methods. 28th international conference, TABLEAUX 2019, London, UK, September 3–5, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11714, 39-57 (2019). MSC: 68T27 68T30 68V15 PDF BibTeX XML Cite \textit{K. Britz} and \textit{I. Varzinczak}, Lect. Notes Comput. Sci. 11714, 39--57 (2019; Zbl 1435.68312) Full Text: DOI OpenURL
Tammet, Tanel GKC: a reasoning system for large knowledge bases. (English) Zbl 07178997 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 538-549 (2019). MSC: 03B35 68V15 PDF BibTeX XML Cite \textit{T. Tammet}, Lect. Notes Comput. Sci. 11716, 538--549 (2019; Zbl 07178997) Full Text: DOI OpenURL
Sternagel, Christian; Winkler, Sarah Certified equational reasoning via ordered completion. (English) Zbl 07178995 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 508-525 (2019). MSC: 03B35 68V15 PDF BibTeX XML Cite \textit{C. Sternagel} and \textit{S. Winkler}, Lect. Notes Comput. Sci. 11716, 508--525 (2019; Zbl 07178995) Full Text: DOI OpenURL
Plaisted, David A. The aspect calculus. (English) Zbl 07178989 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 406-424 (2019). MSC: 03B35 68V15 PDF BibTeX XML Cite \textit{D. A. Plaisted}, Lect. Notes Comput. Sci. 11716, 406--424 (2019; Zbl 07178989) Full Text: DOI OpenURL
Kovács, Zoltán; Pech, Pavel Experiments on automatic inclusion of some non-degeneracy conditions among the hypotheses in locus equation computations. (English) Zbl 1428.68343 Kaliszyk, Cezary (ed.) et al., Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11617, 140-154 (2019). MSC: 68V15 68U05 PDF BibTeX XML Cite \textit{Z. Kovács} and \textit{P. Pech}, Lect. Notes Comput. Sci. 11617, 140--154 (2019; Zbl 1428.68343) Full Text: DOI OpenURL
Alessi, Fabio; Ciaffaglione, Alberto; Di Gianantonio, Pietro; Honsell, Furio; Lenisa, Marina; Scagnetto, Ivan \(\mathrm{LF}^+\) in Coq for fast-and-loose reasoning. (English) Zbl 1427.68344 J. Formaliz. Reason. 12, 11-51 (2019). MSC: 68V15 03B38 03B70 68V20 PDF BibTeX XML Cite \textit{F. Alessi} et al., J. Formaliz. Reason. 12, 11--51 (2019; Zbl 1427.68344) Full Text: DOI OpenURL
Lucas, Salvador Proving semantic properties as first-order satisfiability. (English) Zbl 1478.68356 Artif. Intell. 277, Article ID 103174, 24 p. (2019). MSC: 68T27 68N17 68P15 68Q42 68V15 PDF BibTeX XML Cite \textit{S. Lucas}, Artif. Intell. 277, Article ID 103174, 24 p. (2019; Zbl 1478.68356) Full Text: DOI OpenURL
Li, Zhuang; Liu, Lei; Lü, Shuai; Ren, Junqi Using membrane calculus to describe DPLL algorithm with clause learning. (Chinese. English summary) Zbl 1438.68102 J. Harbin Eng. Univ. 40, No. 4, 799-804 (2019). MSC: 68T05 68Q07 68T20 PDF BibTeX XML Cite \textit{Z. Li} et al., J. Harbin Eng. Univ. 40, No. 4, 799--804 (2019; Zbl 1438.68102) Full Text: DOI OpenURL
Cabalar, Pedro; Costantini, Stefania; De Gasperis, Giovanni; Formisano, Andrea Multi-context systems in dynamic environments. (English) Zbl 1485.68246 Ann. Math. Artif. Intell. 86, No. 1-3, 87-120 (2019). MSC: 68T27 68T30 68T35 68T42 PDF BibTeX XML Cite \textit{P. Cabalar} et al., Ann. Math. Artif. Intell. 86, No. 1--3, 87--120 (2019; Zbl 1485.68246) Full Text: DOI arXiv OpenURL
Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen Automating Event-B invariant proofs by rippling and proof patching. (English) Zbl 1425.68077 Formal Asp. Comput. 31, No. 1, 95-129 (2019). MSC: 68N30 68Q60 68T15 PDF BibTeX XML Cite \textit{Y. Lin} et al., Formal Asp. Comput. 31, No. 1, 95--129 (2019; Zbl 1425.68077) Full Text: DOI OpenURL
Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. (English) Zbl 1395.68246 J. Symb. Comput. 90, 3-41 (2019). MSC: 68T15 68P10 PDF BibTeX XML Cite \textit{I. Drămnesc} et al., J. Symb. Comput. 90, 3--41 (2019; Zbl 1395.68246) Full Text: DOI HAL OpenURL
Pavlov, Vladimir; Pak, Vadim WhaleProver: first-order intuitionistic theorem prover based on the inverse method. (English) Zbl 1461.68247 Petrenko, Alexander K. (ed.) et al., Perspectives of system informatics. 11th international Andrei P. Ershov informatics conference, PSI 2017, Moscow, Russia, June 27–29, 2017. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 10742, 322-336 (2018). MSC: 68V15 03B20 PDF BibTeX XML Cite \textit{V. Pavlov} and \textit{V. Pak}, Lect. Notes Comput. Sci. 10742, 322--336 (2018; Zbl 1461.68247) Full Text: DOI OpenURL
Pozanco, A.; Fernández, S.; Borrajo, D. Learning-driven goal generation. (English) Zbl 1462.68176 AI Commun. 31, No. 2, 137-150 (2018). MSC: 68T20 PDF BibTeX XML Cite \textit{A. Pozanco} et al., AI Commun. 31, No. 2, 137--150 (2018; Zbl 1462.68176) Full Text: DOI OpenURL
Fuentetaja, Raquel; Borrajo, Daniel; de la Rosa, Tomás Anticipation of goals in automated planning. (English) Zbl 1462.68173 AI Commun. 31, No. 2, 117-135 (2018). MSC: 68T20 PDF BibTeX XML Cite \textit{R. Fuentetaja} et al., AI Commun. 31, No. 2, 117--135 (2018; Zbl 1462.68173) Full Text: DOI OpenURL
Recio, Tomás; Sendra, J. Rafael; Villarino, Carlos The importance of being zero. (English) Zbl 1467.13060 Arreche, Carlos (ed.), Proceedings of the 43rd international symposium on symbolic and algebraic computation, ISSAC 2018, New York, NY, USA, July 16–19, 2018. New York, NY: Association for Computing Machinery (ACM). 327-333 (2018). MSC: 13P15 12-08 68W30 PDF BibTeX XML Cite \textit{T. Recio} et al., in: Proceedings of the 43rd international symposium on symbolic and algebraic computation, ISSAC 2018, New York, NY, USA, July 16--19, 2018. New York, NY: Association for Computing Machinery (ACM). 327--333 (2018; Zbl 1467.13060) Full Text: DOI OpenURL
Benzmüller, Christoph; Farjami, Ali; Parent, Xavier A dyadic deontic logic in HOL. (English) Zbl 1418.03069 Broersen, Jan (ed.) et al., Deontic logic and normative systems. 14th international conference, DEON 2018, Utrecht, Netherlands, July 3–6, 2018. Proceedings. London: College Publications. 33-49 (2018). MSC: 03B45 03B15 03B35 PDF BibTeX XML Cite \textit{C. Benzmüller} et al., in: Deontic logic and normative systems. 14th international conference, DEON 2018, Utrecht, Netherlands, July 3--6, 2018. Proceedings. London: College Publications. 33--49 (2018; Zbl 1418.03069) OpenURL
Gleiss, Bernhard; Kovács, Laura; Robillard, Simon Loop analysis by quantification over iterations. (English) Zbl 1415.68146 Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 381-399 (2018). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{B. Gleiss} et al., EPiC Ser. Comput. 57, 381--399 (2018; Zbl 1415.68146) Full Text: DOI OpenURL
Novaro, Arianna; Grandi, Umberto; Herzig, Andreas Judgment aggregation in dynamic logic of propositional assignments. (English) Zbl 1444.03119 J. Log. Comput. 28, No. 7, 1471-1498 (2018). MSC: 03B70 03B45 68T27 91B14 PDF BibTeX XML Cite \textit{A. Novaro} et al., J. Log. Comput. 28, No. 7, 1471--1498 (2018; Zbl 1444.03119) Full Text: DOI Link OpenURL
Hóu, Zhé; Goré, Rajeev; Tiu, Alwen A labelled sequent calculus for BBI: proof theory and proof search. (English) Zbl 1444.03159 J. Log. Comput. 28, No. 4, 809-872 (2018). MSC: 03F03 03B35 03F05 68V15 PDF BibTeX XML Cite \textit{Z. Hóu} et al., J. Log. Comput. 28, No. 4, 809--872 (2018; Zbl 1444.03159) Full Text: DOI arXiv Link OpenURL
Lopez Hernandez, Julio Cesar; Korovin, Konstantin An abstraction-refinement framework for reasoning with large theories. (English) Zbl 06958129 Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 663-679 (2018). MSC: 68T15 PDF BibTeX XML Cite \textit{J. C. Lopez Hernandez} and \textit{K. Korovin}, Lect. Notes Comput. Sci. 10900, 663--679 (2018; Zbl 06958129) Full Text: DOI Link OpenURL
Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina Understanding parameters of deductive verification: an empirical investigation of key. (English) Zbl 06946989 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 342-361 (2018). MSC: 68T15 PDF BibTeX XML Cite \textit{A. Knüppel} et al., Lect. Notes Comput. Sci. 10895, 342--361 (2018; Zbl 06946989) Full Text: DOI OpenURL
Jakubuv, Jan; Kaliszyk, Cezary Towards a unified ordering for superposition-based automated reasoning. (English) Zbl 1395.68248 Davenport, James H. (ed.) et al., Mathematical software – ICMS 2018. 6th international conference, South Bend, IN, USA, July 24–27, 2018. Proceedings. Cham: Springer (ISBN 978-3-319-96417-1/pbk; 978-3-319-96418-8/ebook). Lecture Notes in Computer Science 10931, 245-254 (2018). MSC: 68T15 PDF BibTeX XML Cite \textit{J. Jakubuv} and \textit{C. Kaliszyk}, Lect. Notes Comput. Sci. 10931, 245--254 (2018; Zbl 1395.68248) Full Text: DOI Link OpenURL
Hóu, Zhé; Clouston, Ranald; Goré, Rajeev; Tiu, Alwen Modular labelled sequent calculi for abstract separation logics. (English) Zbl 1407.03046 ACM Trans. Comput. Log. 19, No. 2, Article No. 13, 35 p. (2018). MSC: 03B70 03F03 PDF BibTeX XML Cite \textit{Z. Hóu} et al., ACM Trans. Comput. Log. 19, No. 2, Article No. 13, 35 p. (2018; Zbl 1407.03046) Full Text: DOI arXiv Link OpenURL
Braude, Eric; Abdyldayev, Satbek Generalizing Morley’s and other theorems with automated realization. (English) Zbl 1398.68480 J. Autom. Reasoning 60, No. 4, 503-526 (2018). MSC: 68T15 51M04 PDF BibTeX XML Cite \textit{E. Braude} and \textit{S. Abdyldayev}, J. Autom. Reasoning 60, No. 4, 503--526 (2018; Zbl 1398.68480) Full Text: DOI Link OpenURL
Núñez, Rafael C.; Murthi, Manohar N.; Premaratne, Kamal; Scheutz, Matthias; Bueno, Otávio Uncertain logic processing: logic-based inference and reasoning using Dempster-Shafer models. (English) Zbl 1444.68187 Int. J. Approx. Reasoning 95, 1-21 (2018). MSC: 68T27 68T37 PDF BibTeX XML Cite \textit{R. C. Núñez} et al., Int. J. Approx. Reasoning 95, 1--21 (2018; Zbl 1444.68187) Full Text: DOI OpenURL
Slaney, John; Woltzenlogel Paleo, Bruno Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning. (English) Zbl 1425.68379 J. Autom. Reasoning 60, No. 2, 133-156 (2018). MSC: 68T15 03B35 68T20 PDF BibTeX XML Cite \textit{J. Slaney} and \textit{B. Woltzenlogel Paleo}, J. Autom. Reasoning 60, No. 2, 133--156 (2018; Zbl 1425.68379) Full Text: DOI arXiv OpenURL
Filho, Dimas Melo; Freitas, Fred; Otten, Jens RACCOON: a connection reasoner for the description logic \(\mathcal{ALC}\). (English) Zbl 1403.68262 Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 200-211 (2017). MSC: 68T27 68T30 PDF BibTeX XML Cite \textit{D. M. Filho} et al., EPiC Ser. Comput. 46, 200--211 (2017; Zbl 1403.68262) Full Text: DOI OpenURL
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef TacticToe: learning to reason with HOL4 tactics. (English) Zbl 1403.68224 Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 15-143 (2017). MSC: 68T15 68T05 PDF BibTeX XML Cite \textit{T. Gauthier} et al., EPiC Ser. Comput. 46, 15--143 (2017; Zbl 1403.68224) Full Text: DOI arXiv OpenURL
Kiesl, Benjamin; Suda, Martin; Seidl, Martina; Tompits, Hans; Biere, Armin Blocked clauses in first-order logic. (English) Zbl 1403.68240 Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 31-48 (2017). MSC: 68T20 03B10 68T15 PDF BibTeX XML Cite \textit{B. Kiesl} et al., EPiC Ser. Comput. 46, 31--48 (2017; Zbl 1403.68240) Full Text: DOI arXiv OpenURL
Kovács, Laura; Robillard, Simon; Voronkov, Andrei Coming to terms with quantified reasoning. (English) Zbl 1380.68280 Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 260-270 (2017). MSC: 68Q60 68N30 68T15 PDF BibTeX XML Cite \textit{L. Kovács} et al., in: Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL '17, Paris, France, January 15--21, 2017. New York, NY: Association for Computing Machinery (ACM). 260--270 (2017; Zbl 1380.68280) Full Text: DOI arXiv OpenURL
Pease, Alison; Lawrence, John; Budzynska, Katarzyna; Corneli, Joseph; Reed, Chris Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation. (English) Zbl 1419.68127 Artif. Intell. 246, 181-219 (2017). MSC: 68T27 00A35 68T15 PDF BibTeX XML Cite \textit{A. Pease} et al., Artif. Intell. 246, 181--219 (2017; Zbl 1419.68127) Full Text: DOI OpenURL
Bowles, Juliana; Caminati, Marco B. A verified algorithm enumerating event structures. (English) Zbl 1367.68245 Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 239-254 (2017). MSC: 68T15 05A15 06-04 68Q10 68U35 PDF BibTeX XML Cite \textit{J. Bowles} and \textit{M. B. Caminati}, Lect. Notes Comput. Sci. 10383, 239--254 (2017; Zbl 1367.68245) Full Text: DOI arXiv Link OpenURL
Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno Computer-assisted analysis of the Anderson-Hájek ontological controversy. (English) Zbl 1417.03131 Log. Univers. 11, No. 1, 139-151 (2017). MSC: 03B35 03B15 03B45 PDF BibTeX XML Cite \textit{C. Benzmüller} et al., Log. Univers. 11, No. 1, 139--151 (2017; Zbl 1417.03131) Full Text: DOI OpenURL
Vidal, Amanda MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions. (English) Zbl 1428.68346 Inf. Sci. 372, 709-730 (2016). MSC: 68V15 03B52 PDF BibTeX XML Cite \textit{A. Vidal}, Inf. Sci. 372, 709--730 (2016; Zbl 1428.68346) Full Text: DOI OpenURL
Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, Wolfgang Theorema 2.0: computer-assisted natural-style mathematics. (English) Zbl 1451.68319 J. Formaliz. Reason. 9, No. 1, 149-185 (2016). MSC: 68V15 PDF BibTeX XML Cite \textit{B. Buchberger} et al., J. Formaliz. Reason. 9, No. 1, 149--185 (2016; Zbl 1451.68319) Full Text: DOI OpenURL
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef Hammering towards QED. (English) Zbl 1451.68318 J. Formaliz. Reason. 9, No. 1, 101-148 (2016). MSC: 68V15 PDF BibTeX XML Cite \textit{J. C. Blanchette} et al., J. Formaliz. Reason. 9, No. 1, 101--148 (2016; Zbl 1451.68318) Full Text: DOI OpenURL
Bárcenas, Everardo; Benítez-Guerrero, Edgard; Lavalle, Jesús On regular paths with counting and data tests. (English) Zbl 1394.68108 Arrazola-Ramírez, José Ramón (ed.) et al., Selected papers of the 10th Latin American workshop on logic/languages, algorithms and new methods of reasoning (LANMR), Puebla, Mexico, August 15, 2016. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 328, 3-16 (2016). MSC: 68P15 03B45 68T15 PDF BibTeX XML Cite \textit{E. Bárcenas} et al., Electron. Notes Theor. Comput. Sci. 328, 3--16 (2016; Zbl 1394.68108) Full Text: DOI OpenURL
Chen, Zhuo; Marple, Kyle; Salazar, Elmer; Gupta, Gopal; Tamil, Lakshman A physician advisory system for chronic heart failure management based on knowledge patterns. (English) Zbl 1379.68307 Theory Pract. Log. Program. 16, No. 5-6, 604-618 (2016). MSC: 68T35 68N17 68T30 92C50 PDF BibTeX XML Cite \textit{Z. Chen} et al., Theory Pract. Log. Program. 16, No. 5--6, 604--618 (2016; Zbl 1379.68307) Full Text: DOI arXiv OpenURL
Steen, Alexander; Benzmüller, Christoph Sweet SIXTEEN: automation via embedding into classical higher-order logic. (English) Zbl 1373.03030 Log. Log. Philos. 25, No. 4, 535-554 (2016). Reviewer: Matteo Bianchi (Milano) MSC: 03B50 03B15 PDF BibTeX XML Cite \textit{A. Steen} and \textit{C. Benzmüller}, Log. Log. Philos. 25, No. 4, 535--554 (2016; Zbl 1373.03030) Full Text: DOI OpenURL
Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison Automating change of representation for proofs in discrete mathematics (extended version). (English) Zbl 1409.68261 Math. Comput. Sci. 10, No. 4, 429-457 (2016). MSC: 68T15 68R01 68T27 68T30 PDF BibTeX XML Cite \textit{D. Raggi} et al., Math. Comput. Sci. 10, No. 4, 429--457 (2016; Zbl 1409.68261) Full Text: DOI OpenURL
Chatzikyriakidis, Stergios; Luo, Zhaohui Proof assistants for natural language semantics. (English) Zbl 1483.68456 Amblard, Maxime (ed.) et al., Logical aspects of computational linguistics. Celebrating 20 years of LACL (1996–2016). 9th international conference, LACL 2016, Nancy, France, December 5–7, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10054, 85-98 (2016). MSC: 68T50 68V15 PDF BibTeX XML Cite \textit{S. Chatzikyriakidis} and \textit{Z. Luo}, Lect. Notes Comput. Sci. 10054, 85--98 (2016; Zbl 1483.68456) Full Text: DOI OpenURL
Zhang, Jiafeng; Xu, Yang; Cao, Fasheng The comparability of \(\alpha\)-generalized semantic resolution method based on lattice-valued first-order logic \(\mathrm{LF}(X)\). (Chinese. English summary) Zbl 1363.03011 Fuzzy Syst. Math. 30, No. 1, 146-152 (2016). MSC: 03B52 03B70 68T27 68T37 PDF BibTeX XML Cite \textit{J. Zhang} et al., Fuzzy Syst. Math. 30, No. 1, 146--152 (2016; Zbl 1363.03011) OpenURL
Wang, Hongwei; Liu, Dian; Zhao, Peng; Qi, Chao; Chen, Xi Review on hierarchical task network planning under uncertainty. (Chinese. English summary) Zbl 1363.90001 Acta Autom. Sin. 42, No. 5, 655-667 (2016). MSC: 90-02 68T37 PDF BibTeX XML Cite \textit{H. Wang} et al., Acta Autom. Sin. 42, No. 5, 655--667 (2016; Zbl 1363.90001) Full Text: DOI OpenURL
Steen, Alexander; Wisniewski, Max; Benzmüller, Christoph Agent-based HOL reasoning. (English) Zbl 1434.68646 Greuel, Gert-Martin (ed.) et al., Mathematical software – ICMS 2016. 5th international conference, Berlin, Germany, July 11–14, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9725, 75-81 (2016). MSC: 68V15 03B16 03B35 PDF BibTeX XML Cite \textit{A. Steen} et al., Lect. Notes Comput. Sci. 9725, 75--81 (2016; Zbl 1434.68646) Full Text: DOI Link OpenURL
Jakubův, Jan; Urban, Josef Extending E prover with similarity based clause selection strategies. (English) Zbl 1347.68303 Kohlhase, Michael (ed.) et al., Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-42546-7/pbk; 978-3-319-42547-4/ebook). Lecture Notes in Computer Science 9791. Lecture Notes in Artificial Intelligence, 151-156 (2016). MSC: 68T15 PDF BibTeX XML Cite \textit{J. Jakubův} and \textit{J. Urban}, Lect. Notes Comput. Sci. 9791, 151--156 (2016; Zbl 1347.68303) Full Text: DOI arXiv OpenURL
Maletzky, Alexander Mathematical theory exploration in Theorema: reduction rings. (English) Zbl 1344.68210 Kohlhase, Michael (ed.) et al., Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-42546-7/pbk; 978-3-319-42547-4/ebook). Lecture Notes in Computer Science 9791. Lecture Notes in Artificial Intelligence, 3-17 (2016). MSC: 68T15 13P10 PDF BibTeX XML Cite \textit{A. Maletzky}, Lect. Notes Comput. Sci. 9791, 3--17 (2016; Zbl 1344.68210) Full Text: DOI arXiv OpenURL
Lierler, Yuliya; Truszczynski, Miroslaw On abstract modular inference systems and solvers. (English) Zbl 1357.68230 Artif. Intell. 236, 65-89 (2016). MSC: 68T30 68N17 68T15 68T27 PDF BibTeX XML Cite \textit{Y. Lierler} and \textit{M. Truszczynski}, Artif. Intell. 236, 65--89 (2016; Zbl 1357.68230) Full Text: DOI arXiv OpenURL
Huang, Fangjian Proofs to two inequality conjectures for a point on the plane of a triangle. (English) Zbl 1334.51012 J. Inequal. Appl. 2016, Paper No. 76, 12 p. (2016). MSC: 51M16 51-04 PDF BibTeX XML Cite \textit{F. Huang}, J. Inequal. Appl. 2016, Paper No. 76, 12 p. (2016; Zbl 1334.51012) Full Text: DOI OpenURL
De Giacomo, Giuseppe; Gerevini, Alfonso Emilio; Patrizi, Fabio; Saetti, Alessandro; Sardina, Sebastian Agent planning programs. (English) Zbl 1344.68245 Artif. Intell. 231, 64-106 (2016). MSC: 68T42 68N19 PDF BibTeX XML Cite \textit{G. De Giacomo} et al., Artif. Intell. 231, 64--106 (2016; Zbl 1344.68245) Full Text: DOI OpenURL
Areces, Carlos; Orbe, Ezequiel Symmetries in modal logics. (English) Zbl 1372.03036 Bull. Symb. Log. 21, No. 4, 373-401 (2015). MSC: 03B45 68T15 68T27 PDF BibTeX XML Cite \textit{C. Areces} and \textit{E. Orbe}, Bull. Symb. Log. 21, No. 4, 373--401 (2015; Zbl 1372.03036) Full Text: DOI arXiv OpenURL
Yi, Liu; Yang, Xu; Xiaomei, Zhong Multi-ary \(\alpha\)-semantic resolution automated reasoning based on lattice-valued first-order logic \(\mathrm{LF}(X)\). (English) Zbl 1361.03011 J. Intell. Fuzzy Syst. 29, No. 4, 1581-1593 (2015). MSC: 03B35 68T15 03B52 PDF BibTeX XML Cite \textit{L. Yi} et al., J. Intell. Fuzzy Syst. 29, No. 4, 1581--1593 (2015; Zbl 1361.03011) Full Text: DOI OpenURL
Bulling, Nils; Goranko, Valentin; Jamroga, Wojciech Logics for reasoning about strategic abilities in multi-player games. (English) Zbl 1422.91116 van Benthem, Johan (ed.) et al., Models of strategic reasoning. Logics, games, and communities. Berlin: Springer. Lect. Notes Comput. Sci. 8972, 93-136 (2015). MSC: 91A26 91A20 03B44 PDF BibTeX XML Cite \textit{N. Bulling} et al., Lect. Notes Comput. Sci. 8972, 93--136 (2015; Zbl 1422.91116) Full Text: DOI OpenURL
Urbas, Matej; Jamnik, Mateja; Stapleton, Gem Speedith: a reasoner for spider diagrams. (English) Zbl 1362.68252 J. Logic Lang. Inf. 24, No. 4, 487-540 (2015). MSC: 68T15 68T27 68T30 PDF BibTeX XML Cite \textit{M. Urbas} et al., J. Logic Lang. Inf. 24, No. 4, 487--540 (2015; Zbl 1362.68252) Full Text: DOI Link OpenURL
Kaliszyk, Cezary; Urban, Josef MizAR 40 for Mizar 40. (English) Zbl 1356.68191 J. Autom. Reasoning 55, No. 3, 245-256 (2015). MSC: 68T15 68T05 PDF BibTeX XML Cite \textit{C. Kaliszyk} and \textit{J. Urban}, J. Autom. Reasoning 55, No. 3, 245--256 (2015; Zbl 1356.68191) Full Text: DOI arXiv OpenURL
Pavlov, Vladimir; Pak, Vadim The inverse method application for non-classical logics. (English) Zbl 1346.03036 Nonlinear Phenom. Complex Syst., Minsk 18, No. 2, 181-190 (2015). MSC: 03B35 68T15 03B20 03F55 PDF BibTeX XML Cite \textit{V. Pavlov} and \textit{V. Pak}, Nonlinear Phenom. Complex Syst., Minsk 18, No. 2, 181--190 (2015; Zbl 1346.03036) Full Text: Link OpenURL
Peltier, Nicolas Reasoning on schemas of formulas: an automata-based approach. (English) Zbl 1451.03018 Dediu, Adrian-Horia (ed.) et al., Language and automata theory and applications. 9th international conference, LATA 2015, Nice, France, March 2–6, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8977, 263-274 (2015). MSC: 03B35 03D05 PDF BibTeX XML Cite \textit{N. Peltier}, Lect. Notes Comput. Sci. 8977, 263--274 (2015; Zbl 1451.03018) Full Text: DOI OpenURL
Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare A modal-layered resolution calculus for K. (English) Zbl 1471.03017 De Nivelle, Hans (ed.), Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9323, 185-200 (2015). MSC: 03B35 03B45 68V15 PDF BibTeX XML Cite \textit{C. Nalon} et al., Lect. Notes Comput. Sci. 9323, 185--200 (2015; Zbl 1471.03017) Full Text: DOI OpenURL
Dyckhoff, Roy Invited talk: Coherentisation of first-order logic. (English) Zbl 1471.03016 De Nivelle, Hans (ed.), Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9323, 3-5 (2015). MSC: 03B35 03B10 03B45 03B55 PDF BibTeX XML Cite \textit{R. Dyckhoff}, Lect. Notes Comput. Sci. 9323, 3--5 (2015; Zbl 1471.03016) Full Text: DOI OpenURL
Alama, Jesse; Oppenheimer, Paul E.; Zalta, Edward N. Automating Leibniz’s theory of concepts. (English) Zbl 1465.03049 Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 73-97 (2015). MSC: 03B35 03A05 03B45 68V15 68V20 PDF BibTeX XML Cite \textit{J. Alama} et al., Lect. Notes Comput. Sci. 9195, 73--97 (2015; Zbl 1465.03049) Full Text: DOI Link OpenURL
Plaisted, David A. History and prospects for first-order automated deduction. (English) Zbl 1465.03055 Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 3-28 (2015). MSC: 03B35 03-03 68-03 68V15 PDF BibTeX XML Cite \textit{D. A. Plaisted}, Lect. Notes Comput. Sci. 9195, 3--28 (2015; Zbl 1465.03055) Full Text: DOI OpenURL
Maletzky, Alexander Automated reasoning in reduction rings using the Theorema system. (English) Zbl 1434.13028 Gerdt, Vladimir P. (ed.) et al., Computer algebra in scientific computing. 17th international workshop, CASC 2015, Aachen, Germany, September 14–18, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9301, 307-321 (2015). MSC: 13P10 03B35 68V20 PDF BibTeX XML Cite \textit{A. Maletzky}, Lect. Notes Comput. Sci. 9301, 307--321 (2015; Zbl 1434.13028) Full Text: DOI OpenURL
Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison Automating change of representation for proofs in discrete mathematics. (English) Zbl 1409.68260 Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 227-242 (2015). MSC: 68T15 68R01 68T27 68T30 PDF BibTeX XML Cite \textit{D. Raggi} et al., Lect. Notes Comput. Sci. 9150, 227--242 (2015; Zbl 1409.68260) Full Text: DOI arXiv OpenURL
Sebastiani, Roberto; Tomasi, Silvia Optimization modulo theories with linear rational costs. (English) Zbl 1354.68233 ACM Trans. Comput. Log. 16, No. 2, Article No. 12, 43 p. (2015). MSC: 68T15 68T20 PDF BibTeX XML Cite \textit{R. Sebastiani} and \textit{S. Tomasi}, ACM Trans. Comput. Log. 16, No. 2, Article No. 12, 43 p. (2015; Zbl 1354.68233) Full Text: DOI arXiv Link OpenURL
Omodeo, Eugenio G.; Tomescu, Alexandru I. Set graphs. V. on representing graphs as membership digraphs. (English) Zbl 1331.68203 J. Log. Comput. 25, No. 3, 899-919 (2015). MSC: 68T15 03B35 05C20 05C75 PDF BibTeX XML Cite \textit{E. G. Omodeo} and \textit{A. I. Tomescu}, J. Log. Comput. 25, No. 3, 899--919 (2015; Zbl 1331.68203) Full Text: DOI Link OpenURL