Zheng, Sen; Schmidt, Renate A. Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments. (English) Zbl 07800192 J. Autom. Reasoning 67, No. 4, Paper No. 39, 68 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{S. Zheng} and \textit{R. A. Schmidt}, J. Autom. Reasoning 67, No. 4, Paper No. 39, 68 p. (2023; Zbl 07800192) Full Text: DOI arXiv OA License
Maggesi, Marco; Perini Brogi, Cosimo Mechanising Gödel-Löb provability logic in HOL light. (English) Zbl 07739779 J. Autom. Reasoning 67, No. 3, Paper No. 29, 34 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Maggesi} and \textit{C. Perini Brogi}, J. Autom. Reasoning 67, No. 3, Paper No. 29, 34 p. (2023; Zbl 07739779) Full Text: DOI
Bonacina, Maria Paola; Winkler, Sarah Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover. (English) Zbl 07695709 J. Autom. Reasoning 67, No. 1, Paper No. 6, 42 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{M. P. Bonacina} and \textit{S. Winkler}, J. Autom. Reasoning 67, No. 1, Paper No. 6, 42 p. (2023; Zbl 07695709) Full Text: DOI
Schmoetten, Richard; Palmer, Jake E.; Fleuriot, Jacques D. Towards formalising Schutz’ axioms for Minkowski spacetime in Isabelle/HOL. (English) Zbl 1511.68331 J. Autom. Reasoning 66, No. 4, 953-988 (2022); correction ibid. 67, No. 1, Paper No. 9, 1 p. (2023). MSC: 68V15 68V20 83A05 PDFBibTeX XMLCite \textit{R. Schmoetten} et al., J. Autom. Reasoning 66, No. 4, 953--988 (2022; Zbl 1511.68331) Full Text: DOI arXiv
Steen, Alexander; Benzmüller, Christoph Extensional higher-order paramodulation in Leo-III. (English) Zbl 1509.68321 J. Autom. Reasoning 65, No. 6, 775-807 (2021). MSC: 68V15 03B16 03B35 03B45 PDFBibTeX XMLCite \textit{A. Steen} and \textit{C. Benzmüller}, J. Autom. Reasoning 65, No. 6, 775--807 (2021; Zbl 1509.68321) Full Text: DOI arXiv
Benzmüller, Christoph; Scott, Dana S. Automating free logic in HOL, with an experimental application in category theory. (English) Zbl 1434.68639 J. Autom. Reasoning 64, No. 1, 53-72 (2020). MSC: 68V15 03B16 03B35 03B60 18A15 PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{D. S. Scott}, J. Autom. Reasoning 64, No. 1, 53--72 (2020; Zbl 1434.68639) Full Text: DOI Link
Chihani, Zakaria; Miller, Dale; Renaud, Fabien A semantic framework for proof evidence. (English) Zbl 1425.68371 J. Autom. Reasoning 59, No. 3, 287-330 (2017). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{Z. Chihani} et al., J. Autom. Reasoning 59, No. 3, 287--330 (2017; Zbl 1425.68371) Full Text: DOI HAL
Bonacina, Maria Paola; Johansson, Moa On interpolation in automated theorem proving. (English) Zbl 1315.03018 J. Autom. Reasoning 54, No. 1, 69-97 (2015). MSC: 03B35 68T15 03C40 PDFBibTeX XMLCite \textit{M. P. Bonacina} and \textit{M. Johansson}, J. Autom. Reasoning 54, No. 1, 69--97 (2015; Zbl 1315.03018) Full Text: DOI
Galmiche, Didier; Méry, Daniel A connection-based characterization of bi-intuitionistic validity. (English) Zbl 1314.03030 J. Autom. Reasoning 51, No. 1, 3-26 (2013). MSC: 03B55 03B35 03F05 PDFBibTeX XMLCite \textit{D. Galmiche} and \textit{D. Méry}, J. Autom. Reasoning 51, No. 1, 3--26 (2013; Zbl 1314.03030) Full Text: DOI
Goré, Rajeev; Nguyen, Linh Anh ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching. (English) Zbl 1361.68188 J. Autom. Reasoning 50, No. 4, 355-381 (2013). MSC: 68T15 68T27 68T30 PDFBibTeX XMLCite \textit{R. Goré} and \textit{L. A. Nguyen}, J. Autom. Reasoning 50, No. 4, 355--381 (2013; Zbl 1361.68188) Full Text: DOI
Veroff, R.; Spinks, M. Axiomatizing the skew Boolean propositional calculus. (English) Zbl 1121.03015 J. Autom. Reasoning 37, No. 1-2, 3-20 (2006). MSC: 03B05 03B35 03G99 PDFBibTeX XMLCite \textit{R. Veroff} and \textit{M. Spinks}, J. Autom. Reasoning 37, No. 1--2, 3--20 (2006; Zbl 1121.03015) Full Text: DOI
Arkoudas, Konstantine Simplifying proofs in Fitch-style natural deduction systems. (English) Zbl 1108.03016 J. Autom. Reasoning 34, No. 3, 239-294 (2005). MSC: 03B35 03B10 PDFBibTeX XMLCite \textit{K. Arkoudas}, J. Autom. Reasoning 34, No. 3, 239--294 (2005; Zbl 1108.03016) Full Text: DOI
Lu, James J.; Barback, Monica D.; Henschen, Lawrence J. Interpreting disjunctive logic programs based on a strong sense of disjunction. (English) Zbl 0788.68024 J. Autom. Reasoning 10, No. 3, 345-370 (1993). MSC: 68N17 68P15 PDFBibTeX XMLCite \textit{J. J. Lu} et al., J. Autom. Reasoning 10, No. 3, 345--370 (1993; Zbl 0788.68024) Full Text: DOI
Meyer, Robert K.; Bunder, Martin W.; Powers, Lawrence Implementing the ‘Fool’s model’ of combinatory logic. (English) Zbl 0749.03007 J. Autom. Reasoning 7, No. 4, 597-630 (1991). Reviewer: H.J.Ohlbach (Saarbrücken) MSC: 03B40 03B35 03B47 PDFBibTeX XMLCite \textit{R. K. Meyer} et al., J. Autom. Reasoning 7, No. 4, 597--630 (1991; Zbl 0749.03007) Full Text: DOI
Mints, Grigori; Tammet, Tanel Condensed detachment is complete for relevance logic: A computer-aided proof. (English) Zbl 0751.03011 J. Autom. Reasoning 7, No. 4, 587-596 (1991). Reviewer: G.Mints (Stanford) MSC: 03B47 03B35 68T15 03-04 PDFBibTeX XMLCite \textit{G. Mints} and \textit{T. Tammet}, J. Autom. Reasoning 7, No. 4, 587--596 (1991; Zbl 0751.03011) Full Text: DOI