Gaggl, Sarah Alice; Rudolph, Sebastian; Straß, Hannes On the decomposition of abstract dialectical frameworks and the complexity of naive-based semantics. (English) Zbl 07299927 J. Artif. Intell. Res. (JAIR) 70, 1-64 (2021). MSC: 68T PDF BibTeX XML Cite \textit{S. A. Gaggl} et al., J. Artif. Intell. Res. (JAIR) 70, 1--64 (2021; Zbl 07299927) Full Text: DOI
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: 68T 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
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: 68T PDF BibTeX XML Cite \textit{C. Del Vescovo} et al., J. Artif. Intell. Res. (JAIR) 69, 963--1021 (2020; Zbl 07283370) Full Text: DOI
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: 68T PDF BibTeX XML Cite \textit{C. Benzmüller} et al., Artif. Intell. 287, Article ID 103348, 28 p. (2020; Zbl 07274579) Full Text: DOI
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 07268893 J. Autom. Reasoning 64, No. 6, 1001-1050 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{G. Burel} et al., J. Autom. Reasoning 64, No. 6, 1001--1050 (2020; Zbl 07268893) Full Text: DOI
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 07261571 Bull. Sect. Log., Univ. Łódź, Dep. Log. 49, No. 2, 127-148 (2020). MSC: 03 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 07261571) Full Text: DOI
Kirchner, Daniel; Benzmüller, Christoph; Zalta, Edward N. Mechanizing Principia Logico-Metaphysica in functional type-theory. (English) Zbl 07181947 Rev. Symb. Log. 13, No. 1, 206-218 (2020). MSC: 03A05 03B35 03B45 03B60 03B80 68V15 68T27 68T30 PDF BibTeX XML Cite \textit{D. Kirchner} et al., Rev. Symb. Log. 13, No. 1, 206--218 (2020; Zbl 07181947) Full Text: DOI
Baumgartner, Peter; Schmidt, Renate A. Blocking and other enhancements for bottom-up model generation methods. (English) Zbl 07176597 J. Autom. Reasoning 64, No. 2, 197-251 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Baumgartner} and \textit{R. A. Schmidt}, J. Autom. Reasoning 64, No. 2, 197--251 (2020; Zbl 07176597) Full Text: DOI
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
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
Huang, Pei; Liu, Minghao; Ge, Cunjing; Ma, Feifei; Zhang, Jian Investigating the existence of orthogonal golf designs via satisfiability testing. (English) Zbl 07246248 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) (ISBN 978-1-4503-6084-5). 203-210 (2019). MSC: 68W30 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 07246248) Full Text: DOI
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
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
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 (ISBN 978-3-030-29435-9/pbk; 978-3-030-29436-6/ebook). Lecture Notes in Computer Science 11716. Lecture Notes in Artificial Intelligence, 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
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 (ISBN 978-3-030-29435-9/pbk; 978-3-030-29436-6/ebook). Lecture Notes in Computer Science 11716. Lecture Notes in Artificial Intelligence, 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
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 (ISBN 978-3-030-29435-9/pbk; 978-3-030-29436-6/ebook). Lecture Notes in Computer Science 11716. Lecture Notes in Artificial Intelligence, 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
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
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, No. 1, 11-51 (2019). MSC: 68V15 03B38 03B70 68V20 PDF BibTeX XML Cite \textit{F. Alessi} et al., J. Formaliz. Reason. 12, No. 1, 11--51 (2019; Zbl 1427.68344) Full Text: DOI
Lucas, Salvador Proving semantic properties as first-order satisfiability. (English) Zbl 07153688 Artif. Intell. 277, Article ID 103174, 24 p. (2019). MSC: 68T PDF BibTeX XML Cite \textit{S. Lucas}, Artif. Intell. 277, Article ID 103174, 24 p. (2019; Zbl 07153688) Full Text: DOI
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
Cabalar, Pedro; Costantini, Stefania; De Gasperis, Giovanni; Formisano, Andrea Multi-context systems in dynamic environments. (English) Zbl 07093480 Ann. Math. Artif. Intell. 86, No. 1-3, 87-120 (2019). MSC: 68T42 68T30 68T35 68T27 PDF BibTeX XML Cite \textit{P. Cabalar} et al., Ann. Math. Artif. Intell. 86, No. 1--3, 87--120 (2019; Zbl 07093480) Full Text: DOI
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
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
Recio, Tomás; Sendra, J. Rafael; Villarino, Carlos The importance of being zero. (English) Zbl 07245533 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) (ISBN 978-1-4503-5550-6). 327-333 (2018). MSC: 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 07245533) Full Text: DOI
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)
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
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
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
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 (ISBN 978-3-319-94204-9/pbk; 978-3-319-94205-6/ebook). Lecture Notes in Computer Science 10900. Lecture Notes in Artificial Intelligence, 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
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 (ISBN 978-3-319-94820-1/pbk; 978-3-319-94821-8/ebook). Lecture Notes in Computer Science 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
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
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, Paper 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, Paper No. 13, 35 p. (2018; Zbl 1407.03046) Full Text: DOI
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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)
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare A modal-layered resolution calculus for K. (English) Zbl 06519942 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 (ISBN 978-3-319-24311-5/pbk; 978-3-319-24312-2/ebook). Lecture Notes in Computer Science 9323. Lecture Notes in Artificial Intelligence., 185-200 (2015). MSC: 68T15 PDF BibTeX XML Cite \textit{C. Nalon} et al., Lect. Notes Comput. Sci. 9323, 185--200 (2015; Zbl 06519942) Full Text: DOI
Dyckhoff, Roy Invited talk: coherentisation of first-order logic. (English) Zbl 06519930 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 (ISBN 978-3-319-24311-5/pbk; 978-3-319-24312-2/ebook). Lecture Notes in Computer Science 9323. Lecture Notes in Artificial Intelligence., 3-5 (2015). MSC: 68T15 PDF BibTeX XML Cite \textit{R. Dyckhoff}, Lect. Notes Comput. Sci. 9323, 3--5 (2015; Zbl 06519930) Full Text: DOI
Alama, Jesse; Oppenheimer, Paul E.; Zalta, Edward N. Automating Leibniz’s theory of concepts. (English) Zbl 06515498 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 (ISBN 978-3-319-21400-9/pbk; 978-3-319-21401-6/ebook). Lecture Notes in Computer Science 9195. Lecture Notes in Artificial Intelligence, 73-97 (2015). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{J. Alama} et al., Lect. Notes Comput. Sci. 9195, 73--97 (2015; Zbl 06515498) Full Text: DOI
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
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
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
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
Mummert, Carl; Saadaoui, Alaeddine; Sovine, Sean The modal logic of reverse mathematics. (English) Zbl 1369.03102 Arch. Math. Logic 54, No. 3-4, 425-437 (2015). MSC: 03B30 03B45 PDF BibTeX XML Cite \textit{C. Mummert} et al., Arch. Math. Logic 54, No. 3--4, 425--437 (2015; Zbl 1369.03102) Full Text: DOI arXiv
Kaliszyk, Cezary; Urban, Josef HOL(y)Hammer: online ATP service for HOL Light. (English) Zbl 1322.68177 Math. Comput. Sci. 9, No. 1, 5-22 (2015). MSC: 68T15 68T05 68T20 68T35 PDF BibTeX XML Cite \textit{C. Kaliszyk} and \textit{J. Urban}, Math. Comput. Sci. 9, No. 1, 5--22 (2015; Zbl 1322.68177) Full Text: DOI
Nguyen, Thi-Minh-Tam; Vu, Viet-Trung; Doan, The-Vinh; Tran, Duc-Khanh Resolution in linguistic first order logic based on linear symmetrical hedge algebra. (English) Zbl 1419.68125 Laurent, Anne (ed.) et al., Information processing and management of uncertainty in knowledge-based systems. 15th international conference, IPMU 2014, Montpellier, France, July 15–19, 2014. Proceedings. Part I. Cham: Springer. Commun. Comput. Inf. Sci. 442, 345-354 (2014). MSC: 68T27 68T15 PDF BibTeX XML Cite \textit{T.-M.-T. Nguyen} et al., Commun. Comput. Inf. Sci. 442, 345--354 (2014; Zbl 1419.68125) Full Text: DOI
Zhong, Xiaomei; Xu, Yang \(\alpha\)-group quasi-lock semantic resolution method based on lattice-valued propositional logic \(LP(X)\). (English) Zbl 1394.03079 J. Mult.-Val. Log. Soft Comput. 22, No. 4-6, 581-598 (2014). MSC: 03G25 03B50 03B52 PDF BibTeX XML Cite \textit{X. Zhong} and \textit{Y. Xu}, J. Mult.-Val. Log. Soft Comput. 22, No. 4--6, 581--598 (2014; Zbl 1394.03079) Full Text: Link
Shen, Yuping; Zhao, Xishun Proof systems for planning under 0-approximation semantics. (English) Zbl 1343.68222 Sci. China, Inf. Sci. 57, No. 7, Article ID 072108, 12 p. (2014). MSC: 68T20 PDF BibTeX XML Cite \textit{Y. Shen} and \textit{X. Zhao}, Sci. China, Inf. Sci. 57, No. 7, Article ID 072108, 12 p. (2014; Zbl 1343.68222) Full Text: DOI
Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef Premise selection for mathematics by corpus analysis and kernel methods. (English) Zbl 1315.68217 J. Autom. Reasoning 52, No. 2, 191-213 (2014). MSC: 68T15 68T05 PDF BibTeX XML Cite \textit{J. Alama} et al., J. Autom. Reasoning 52, No. 2, 191--213 (2014; Zbl 1315.68217) Full Text: DOI
Omodeo, Eugenio G.; Tomescu, Alexandru I. Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets. (English) Zbl 1315.68223 J. Autom. Reasoning 52, No. 1, 1-29 (2014). MSC: 68T15 03B35 05C75 PDF BibTeX XML Cite \textit{E. G. Omodeo} and \textit{A. I. Tomescu}, J. Autom. Reasoning 52, No. 1, 1--29 (2014; Zbl 1315.68223) Full Text: DOI
Nguyen, Linh Anh; Golińska-Pilarek, Joanna An ExpTime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic SHOQ. (English) Zbl 1315.68231 Fundam. Inform. 135, No. 4, 433-449 (2014). MSC: 68T27 03B35 68T15 68T30 PDF BibTeX XML Cite \textit{L. A. Nguyen} and \textit{J. Golińska-Pilarek}, Fundam. Inform. 135, No. 4, 433--449 (2014; Zbl 1315.68231) Full Text: DOI
Kaliszyk, Cezary; Urban, Josef Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). (English) Zbl 1314.68283 J. Autom. Reasoning 53, No. 2, 173-213 (2014); erratum ibid. 54, No. 1, 99 (2015). MSC: 68T15 68T05 PDF BibTeX XML Cite \textit{C. Kaliszyk} and \textit{J. Urban}, J. Autom. Reasoning 53, No. 2, 173--213 (2014; Zbl 1314.68283) Full Text: DOI
Liu, Qiang; Ma, Jiachen; Xie, Wei; Ma, Liyong Multi-robot learning using a PSO combined with CBR algorithm. (English) Zbl 1313.68110 J. Univ. Electron. Sci. Technol. China 43, No. 1, 137-143 (2014). MSC: 68T05 68T20 68T40 93C85 PDF BibTeX XML Cite \textit{Q. Liu} et al., J. Univ. Electron. Sci. Technol. China 43, No. 1, 137--143 (2014; Zbl 1313.68110) Full Text: DOI
Chatterjee, Siddharth; Sen, Arunava Automated reasoning in social choice theory: some remarks. (English) Zbl 1302.91077 Math. Comput. Sci. 8, No. 1, 5-10 (2014). MSC: 91B14 68T15 03B35 PDF BibTeX XML Cite \textit{S. Chatterjee} and \textit{A. Sen}, Math. Comput. Sci. 8, No. 1, 5--10 (2014; Zbl 1302.91077) Full Text: DOI
Nikitina, Nadeschda; Rudolph, Sebastian (Non-)succinctness of uniform interpolants of general terminologies in the description logic \(\mathcal{EL}\). (English) Zbl 1308.68110 Artif. Intell. 215, 120-140 (2014). MSC: 68T27 68T15 68T30 PDF BibTeX XML Cite \textit{N. Nikitina} and \textit{S. Rudolph}, Artif. Intell. 215, 120--140 (2014; Zbl 1308.68110) Full Text: DOI
Jin, Xin; Ray, Asok Navigation of autonomous vehicles for oil spill cleaning in dynamic and uncertain environments. (English) Zbl 1322.93073 Int. J. Control 87, No. 4, 787-801 (2014). MSC: 93C85 68T40 68T37 PDF BibTeX XML Cite \textit{X. Jin} and \textit{A. Ray}, Int. J. Control 87, No. 4, 787--801 (2014; Zbl 1322.93073) Full Text: DOI
Hóu, Zhé; Clouston, Ranald; Goré, Rajeev; Tiu, Alwen Proof search for propositional abstract separation logics via labelled sequents. (English) Zbl 1284.68402 Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 465-476 (2014). MSC: 68Q60 03B70 68T15 PDF BibTeX XML Cite \textit{Z. Hóu} et al., in: Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '14, San Diego, CA, USA, January 22--24, 2014. New York, NY: Association for Computing Machinery (ACM). 465--476 (2014; Zbl 1284.68402) Full Text: DOI
Gasquet, Olivier; Herzig, Andreas; Said, Bilal; Schwarzentruber, François Kripke’s worlds. An introduction to modal logics via tableaux. (English) Zbl 1280.03001 Studies in Universal Logic. Basel: Birkhäuser/Springer (ISBN 978-3-7643-8503-3/pbk; 978-3-7643-8504-0/ebook). xv, 198 p. (2014). Reviewer: Andrzej Indrzejczak (Łódź) MSC: 03-01 03B35 03B42 03B45 05C90 68Q60 68T15 PDF BibTeX XML Cite \textit{O. Gasquet} et al., Kripke's worlds. An introduction to modal logics via tableaux. Basel: Birkhäuser/Springer (2014; Zbl 1280.03001) Full Text: DOI
Chan, Hing Lun; Norrish, Michael A string of pearls: proofs of Fermat’s little theorem. (English) Zbl 1451.68320 J. Formaliz. Reason. 6, No. 1, 63-87 (2013). MSC: 68V15 11A07 PDF BibTeX XML Cite \textit{H. L. Chan} and \textit{M. Norrish}, J. Formaliz. Reason. 6, No. 1, 63--87 (2013; Zbl 1451.68320) Full Text: DOI
Cerrito, Serenella; Mayer, Marta Cialdea A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities. (English) Zbl 1314.03018 J. Autom. Reasoning 51, No. 2, 197-239 (2013). MSC: 03B35 03B45 03B62 PDF BibTeX XML Cite \textit{S. Cerrito} and \textit{M. C. Mayer}, J. Autom. Reasoning 51, No. 2, 197--239 (2013; Zbl 1314.03018) Full Text: DOI
Indrzejczak, Andrzej; Zawidzki, Michał Decision procedures for some strong hybrid logics. (English) Zbl 1321.03031 Log. Log. Philos. 22, No. 4, 389-409 (2013). MSC: 03B45 03B35 PDF BibTeX XML Cite \textit{A. Indrzejczak} and \textit{M. Zawidzki}, Log. Log. Philos. 22, No. 4, 389--409 (2013; Zbl 1321.03031)
Fiala, Nick C. A still shorter axiom for trimedial quasigroups. (English) Zbl 1294.20076 Quasigroups Relat. Syst. 21, No. 2, 203-206 (2013). MSC: 20N05 20A05 68T15 PDF BibTeX XML Cite \textit{N. C. Fiala}, Quasigroups Relat. Syst. 21, No. 2, 203--206 (2013; Zbl 1294.20076)
Fiala, Nick C.; Agre, Keith M. Shortest single axioms with neutral element for groups of exponent 2 and 3. (English) Zbl 1293.68249 Quasigroups Relat. Syst. 21, No. 1, 69-82 (2013); errata ibid. 22, No. 2, 301-302 (2014). MSC: 68T15 68W30 20A05 20N02 PDF BibTeX XML Cite \textit{N. C. Fiala} and \textit{K. M. Agre}, Quasigroups Relat. Syst. 21, No. 1, 69--82 (2013; Zbl 1293.68249) Full Text: Link
Grandi, Umberto; Endriss, Ulle First-order logic formalisation of impossibility theorems in preference aggregation. (English) Zbl 1285.91041 J. Philos. Log. 42, No. 4, 595-618 (2013). Reviewer: H. C. M. de Swart (Tilburg) MSC: 91B14 91B12 03B80 03B35 PDF BibTeX XML Cite \textit{U. Grandi} and \textit{U. Endriss}, J. Philos. Log. 42, No. 4, 595--618 (2013; Zbl 1285.91041) Full Text: DOI
Zuo, Ming; Haarslev, Volker Intelligent tableau algorithm for DL reasoning. (English) Zbl 1401.68281 Galmiche, Didier (ed.) et al., Automated reasoning with analytic tableaux and related methods. 22nd international conference, TABLEAUX 2013, Nancy, France, September 16–19, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40536-5/pbk). Lecture Notes in Computer Science 8123. Lecture Notes in Artificial Intelligence, 273-287 (2013). MSC: 68T15 68T05 68T27 PDF BibTeX XML Cite \textit{M. Zuo} and \textit{V. Haarslev}, Lect. Notes Comput. Sci. 8123, 273--287 (2013; Zbl 1401.68281) Full Text: DOI
Bofill, Miquel; Rubio, Albert Paramodulation with non-monotonic orderings and simplification. (English) Zbl 1315.03017 J. Autom. Reasoning 50, No. 1, 51-98 (2013). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{M. Bofill} and \textit{A. Rubio}, J. Autom. Reasoning 50, No. 1, 51--98 (2013; Zbl 1315.03017) Full Text: DOI
Ireland, Andrew; Grov, Gudmund; Llano, Maria Teresa; Butler, Michael Reasoned modelling critics: turning failed proofs into modelling guidance. (English) Zbl 1264.68058 Sci. Comput. Program. 78, No. 3, 293-309 (2013). MSC: 68N30 68T20 PDF BibTeX XML Cite \textit{A. Ireland} et al., Sci. Comput. Program. 78, No. 3, 293--309 (2013; Zbl 1264.68058) Full Text: DOI
Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff ATP and presentation service for Mizar formalizations. (English) Zbl 1260.68380 J. Autom. Reasoning 50, No. 2, 229-241 (2013). MSC: 68T15 PDF BibTeX XML Cite \textit{J. Urban} et al., J. Autom. Reasoning 50, No. 2, 229--241 (2013; Zbl 1260.68380) Full Text: DOI
van Ditmarsch, Hans; Herzig, Andreas; de Lima, Tiago Public announcements, public assignments and the complexity of their logic. (English) Zbl 1398.03076 J. Appl. Non-Class. Log. 22, No. 3, 249-273 (2012). MSC: 03B42 68T27 68Q17 PDF BibTeX XML Cite \textit{H. van Ditmarsch} et al., J. Appl. Non-Class. Log. 22, No. 3, 249--273 (2012; Zbl 1398.03076) Full Text: DOI
Constable, Robert L. On building constructive formal theories of computation noting the roles of Turing, Church, and Brouwer. (English) Zbl 1362.68250 Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25–28, 2012. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-4769-5). 2-8 (2012). MSC: 68T15 68-03 PDF BibTeX XML Cite \textit{R. L. Constable}, in: Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25--28, 2012. Los Alamitos, CA: IEEE Computer Society. 2--8 (2012; Zbl 1362.68250) Full Text: DOI
Slaney, John Visualising reasoning: what ATP can learn from CP. (English) Zbl 1294.68127 Aspinall, David (ed.) et al., Proceedings of the 9th international workshop on user interfaces for theorem provers (UITP10), Edinburgh, UK, July 15, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 285, 57-70 (2012). MSC: 68T15 68U35 PDF BibTeX XML Cite \textit{J. Slaney}, Electron. Notes Theor. Comput. Sci. 285, 57--70 (2012; Zbl 1294.68127) Full Text: DOI
Xu, Wei-tao; Xu, Yang Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra. (English) Zbl 1283.03091 J. Shanghai Jiaotong Univ., Sci. 17, No. 2, 178-181 (2012). MSC: 03G10 03B35 03B52 PDF BibTeX XML Cite \textit{W.-t. Xu} and \textit{Y. Xu}, J. Shanghai Jiaotong Univ., Sci. 17, No. 2, 178--181 (2012; Zbl 1283.03091) Full Text: DOI