Padmanabha, Anantha; Ramanujam, R. A decidable fragment of first order modal logic: two variable term modal logic. (English) Zbl 07760990 ACM Trans. Comput. Log. 24, No. 4, Paper No. 29, 38 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{A. Padmanabha} and \textit{R. Ramanujam}, ACM Trans. Comput. Log. 24, No. 4, Paper No. 29, 38 p. (2023; Zbl 07760990) Full Text: DOI
Barthe, Gilles; Jacomme, Charlie; Kremer, Steve Universal equivalence and majority of probabilistic programs over finite fields. (English) Zbl 1508.68215 ACM Trans. Comput. Log. 23, No. 1, Article No. 5, 42 p. (2021). MSC: 68Q60 11Y16 68N30 68P27 94A60 PDFBibTeX XMLCite \textit{G. Barthe} et al., ACM Trans. Comput. Log. 23, No. 1, Article No. 5, 42 p. (2021; Zbl 1508.68215) Full Text: DOI
van der Meyden, Ron; Patra, Manas K. Undecidable cases of model checking probabilistic temporal-epistemic logic. (English) Zbl 1502.68188 ACM Trans. Comput. Log. 21, No. 4, Article No. 32, 26 p. (2020). MSC: 68Q60 03B42 03B44 PDFBibTeX XMLCite \textit{R. van der Meyden} and \textit{M. K. Patra}, ACM Trans. Comput. Log. 21, No. 4, Article No. 32, 26 p. (2020; Zbl 1502.68188) Full Text: DOI arXiv
Balbiani, Philippe; Boudou, Joseph; Diéguez, Martín; Fernández-Duque, David Intuitionistic linear temporal logics. (English) Zbl 1433.03047 ACM Trans. Comput. Log. 21, No. 2, Article No. 14, 32 p. (2020). MSC: 03B44 03B20 03B47 03B25 PDFBibTeX XMLCite \textit{P. Balbiani} et al., ACM Trans. Comput. Log. 21, No. 2, Article No. 14, 32 p. (2020; Zbl 1433.03047) Full Text: DOI arXiv Link
Feng, Shiguang; Carapelle, Claudia; Gil, Oliver Fernández; Quaas, Karin MTL and TPTL for one-counter machines. Expressiveness, model checking, and satisfiability. (English) Zbl 1433.68215 ACM Trans. Comput. Log. 21, No. 2, Article No. 12, 34 p. (2020). MSC: 68Q60 03B25 03B44 PDFBibTeX XMLCite \textit{S. Feng} et al., ACM Trans. Comput. Log. 21, No. 2, Article No. 12, 34 p. (2020; Zbl 1433.68215) Full Text: DOI
Kieroński, Emanuel; Tendera, Lidia Finite satisfiability of the two-variable guarded fragment with transitive guards and related variants. (English) Zbl 1407.03009 ACM Trans. Comput. Log. 19, No. 2, Article No. 8, 34 p. (2018). MSC: 03B25 03C13 68Q25 PDFBibTeX XMLCite \textit{E. Kieroński} and \textit{L. Tendera}, ACM Trans. Comput. Log. 19, No. 2, Article No. 8, 34 p. (2018; Zbl 1407.03009) Full Text: DOI arXiv
Eickmeyer, Kord; Elberfeld, Michael; Harwath, Frederik Succinctness of order-invariant logics on depth-bounded structures. (English) Zbl 1407.03002 ACM Trans. Comput. Log. 18, No. 4, Article No. 33, 25 p. (2017). MSC: 03B10 03B15 03B25 PDFBibTeX XMLCite \textit{K. Eickmeyer} et al., ACM Trans. Comput. Log. 18, No. 4, Article No. 33, 25 p. (2017; Zbl 1407.03002) Full Text: DOI arXiv
Krebs, Andreas; Straubing, Howard An effective characterization of the alternation hierarchy in two-variable logic. (English) Zbl 1407.03054 ACM Trans. Comput. Log. 18, No. 4, Article No. 30, 22 p. (2017). MSC: 03D05 03B20 03B25 03C07 PDFBibTeX XMLCite \textit{A. Krebs} and \textit{H. Straubing}, ACM Trans. Comput. Log. 18, No. 4, Article No. 30, 22 p. (2017; Zbl 1407.03054) Full Text: DOI Link
Radcliffe, Nicholas R.; Moraes, Luis F. T.; Verma, Rakesh M. Uniqueness of normal forms for shallow term rewrite systems. (English) Zbl 1367.68149 ACM Trans. Comput. Log. 18, No. 2, Article No. 17, 20 p. (2017). MSC: 68Q42 PDFBibTeX XMLCite \textit{N. R. Radcliffe} et al., ACM Trans. Comput. Log. 18, No. 2, Article No. 17, 20 p. (2017; Zbl 1367.68149) Full Text: DOI arXiv
Michaliszyn, Jakub; Otop, Jan; Kieroński, Emanuel On the decidability of elementary modal logics. (English) Zbl 1367.03043 ACM Trans. Comput. Log. 17, No. 1, Article No. 2, 47 p. (2015). MSC: 03B45 03B25 68Q17 68Q25 PDFBibTeX XMLCite \textit{J. Michaliszyn} et al., ACM Trans. Comput. Log. 17, No. 1, Article No. 2, 47 p. (2015; Zbl 1367.03043) Full Text: DOI
Hampson, Christopher; Kurucz, Agi Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting. (English) Zbl 1354.03022 ACM Trans. Comput. Log. 16, No. 3, Article No. 27, 36 p. (2015). MSC: 03B44 03B25 03B45 03D05 PDFBibTeX XMLCite \textit{C. Hampson} and \textit{A. Kurucz}, ACM Trans. Comput. Log. 16, No. 3, Article No. 27, 36 p. (2015; Zbl 1354.03022) Full Text: DOI arXiv
Benerecetti, Massimo; Mogavero, Fabio; Murano, Aniello Reasoning about substructures and games. (English) Zbl 1354.03019 ACM Trans. Comput. Log. 16, No. 3, Article No. 25, 51 p. (2015). MSC: 03B44 03B25 68Q60 PDFBibTeX XMLCite \textit{M. Benerecetti} et al., ACM Trans. Comput. Log. 16, No. 3, Article No. 25, 51 p. (2015; Zbl 1354.03019) Full Text: DOI
Demri, Stéphane; Deters, Morgan Two-variable separation logic and its inner circle. (English) Zbl 1354.03036 ACM Trans. Comput. Log. 16, No. 2, Article No. 15, 36 p. (2015). MSC: 03B70 03B25 PDFBibTeX XMLCite \textit{S. Demri} and \textit{M. Deters}, ACM Trans. Comput. Log. 16, No. 2, Article No. 15, 36 p. (2015; Zbl 1354.03036) Full Text: DOI HAL
Biscaia, M.; Henriques, D.; Mateus, P. Decidability of approximate Skolem problem and applications to logical verification of dynamical properties of Markov chains. (English) Zbl 1354.68168 ACM Trans. Comput. Log. 16, No. 1, Article No. 4, 17 p. (2015). MSC: 68Q60 03B25 03B44 11U05 60J20 68Q87 PDFBibTeX XMLCite \textit{M. Biscaia} et al., ACM Trans. Comput. Log. 16, No. 1, Article No. 4, 17 p. (2015; Zbl 1354.68168) Full Text: DOI
Boker, Udi; Chatterjee, Krishnendu; Henzinger, Thomas A.; Kupferman, Orna Temporal specifications with accumulative values. (English) Zbl 1354.68169 ACM Trans. Comput. Log. 15, No. 4, Article No. 27, 25 p. (2014). MSC: 68Q60 03B25 03B44 PDFBibTeX XMLCite \textit{U. Boker} et al., ACM Trans. Comput. Log. 15, No. 4, Article No. 27, 25 p. (2014; Zbl 1354.68169) Full Text: DOI
Schmidt, Renate A.; Tishkovsky, Dmitry Using tableau to decide description logics with full role negation and identity. (English) Zbl 1287.03031 ACM Trans. Comput. Log. 15, No. 1, Article No. 7, 31 p. (2014). MSC: 03B35 03B45 68T27 PDFBibTeX XMLCite \textit{R. A. Schmidt} and \textit{D. Tishkovsky}, ACM Trans. Comput. Log. 15, No. 1, Article No. 7, 31 p. (2014; Zbl 1287.03031) Full Text: DOI arXiv
Kartzow, Alexander First-order logic on higher-order nested pushdown trees. (English) Zbl 1353.68053 ACM Trans. Comput. Log. 14, No. 2, Article No. 8, 45 p. (2013). MSC: 68N30 03B70 68Q45 68Q60 PDFBibTeX XMLCite \textit{A. Kartzow}, ACM Trans. Comput. Log. 14, No. 2, Article No. 8, 45 p. (2013; Zbl 1353.68053) Full Text: DOI arXiv
Larchey-Wendling, Dominique; Galmiche, Didier Nondeterministic phase semantics and the undecidability of Boolean BI. (English) Zbl 1343.03022 ACM Trans. Comput. Log. 14, No. 1, Article No. 6, 41 p. (2013). MSC: 03B47 03B25 03B70 03D05 PDFBibTeX XMLCite \textit{D. Larchey-Wendling} and \textit{D. Galmiche}, ACM Trans. Comput. Log. 14, No. 1, Article No. 6, 41 p. (2013; Zbl 1343.03022) Full Text: DOI HAL
Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido Simplification rules for intuitionistic propositional tableaux. (English) Zbl 1352.03015 ACM Trans. Comput. Log. 13, No. 2, Article No. 14, 23 p. (2012). MSC: 03B35 03B20 03B25 68T15 PDFBibTeX XMLCite \textit{M. Ferrari} et al., ACM Trans. Comput. Log. 13, No. 2, Article No. 14, 23 p. (2012; Zbl 1352.03015) Full Text: DOI Link
Bojańczyk, Mikołaj; David, Claire; Muscholl, Anca; Schwentick, Thomas; Segoufin, Luc Two-variable logic on data words. (English) Zbl 1352.03041 ACM Trans. Comput. Log. 12, No. 4, Article No. 27, 26 p. (2011). MSC: 03B70 03B25 68Q85 PDFBibTeX XMLCite \textit{M. Bojańczyk} et al., ACM Trans. Comput. Log. 12, No. 4, Article No. 27, 26 p. (2011; Zbl 1352.03041) Full Text: DOI
Jurdziński, Marcin; Lazić, Ranko Alternating automata on data trees and XPath satisfiability. (English) Zbl 1351.68141 ACM Trans. Comput. Log. 12, No. 3, Article No. 19, 21 p. (2011). MSC: 68Q45 03B25 68P15 PDFBibTeX XMLCite \textit{M. Jurdziński} and \textit{R. Lazić}, ACM Trans. Comput. Log. 12, No. 3, Article No. 19, 21 p. (2011; Zbl 1351.68141) Full Text: DOI arXiv
Lazić, Ranko Safety alternating automata on data words. (English) Zbl 1352.03014 ACM Trans. Comput. Log. 12, No. 2, Article No. 10, 24 p. (2011). MSC: 03B25 03B44 03D05 68Q25 PDFBibTeX XMLCite \textit{R. Lazić}, ACM Trans. Comput. Log. 12, No. 2, Article No. 10, 24 p. (2011; Zbl 1352.03014) Full Text: DOI arXiv
Kähler, Detlef; Küsters, Ralf; Wilke, Thomas Deciding strategy properties of contract-signing protocols. (English) Zbl 1351.94053 ACM Trans. Comput. Log. 11, No. 3, Article No. 17, 42 p. (2010). MSC: 94A60 91A80 94A62 PDFBibTeX XMLCite \textit{D. Kähler} et al., ACM Trans. Comput. Log. 11, No. 3, Article No. 17, 42 p. (2010; Zbl 1351.94053) Full Text: DOI
Bailey, James; Dong, Guozhu; To, Anthony Widjaja Logical queries over views, decidability and expressiveness. (English) Zbl 1351.68087 ACM Trans. Comput. Log. 11, No. 2, Article No. 8, 35 p. (2010). MSC: 68P15 03B25 03B70 PDFBibTeX XMLCite \textit{J. Bailey} et al., ACM Trans. Comput. Log. 11, No. 2, Article No. 8, 35 p. (2010; Zbl 1351.68087) Full Text: DOI
Goranko, Valentin; Shkatov, Dmitry Tableau-based decision procedures for logics of strategic ability in multiagent systems. (English) Zbl 1351.68266 ACM Trans. Comput. Log. 11, No. 1, Article No. 3, 51 p. (2009). MSC: 68T27 03B25 03B44 68T42 PDFBibTeX XMLCite \textit{V. Goranko} and \textit{D. Shkatov}, ACM Trans. Comput. Log. 11, No. 1, Article No. 3, 51 p. (2009; Zbl 1351.68266) Full Text: DOI arXiv
Giordano, Laura; Gliozzi, Valentina; Olivetti, Nicola; Pozzato, Gian Luca Analytic tableaux calculi for KLM logics of nonmonotonic reasoning. (English) Zbl 1351.03004 ACM Trans. Comput. Log. 10, No. 3, Article No. 18, 47 p. (2009). MSC: 03B35 03B25 03B45 03B60 68Q25 PDFBibTeX XMLCite \textit{L. Giordano} et al., ACM Trans. Comput. Log. 10, No. 3, Article No. 18, 47 p. (2009; Zbl 1351.03004) Full Text: DOI arXiv
Demri, Stéphane; Lazić, Ranko LTL with the freeze quantifier and register automata. (English) Zbl 1351.68158 ACM Trans. Comput. Log. 10, No. 3, Article No. 16, 30 p. (2009). MSC: 68Q60 03B25 03B44 68Q45 PDFBibTeX XMLCite \textit{S. Demri} and \textit{R. Lazić}, ACM Trans. Comput. Log. 10, No. 3, Article No. 16, 30 p. (2009; Zbl 1351.68158) Full Text: DOI
Wolter, Frank; Zakharyaschev, Michael Undecidability of the unification and admissibility problems for modal and description logics. (English) Zbl 1367.03026 ACM Trans. Comput. Log. 9, No. 4, Article No. 25, 20 p. (2008). MSC: 03B35 03B25 03B45 68T27 PDFBibTeX XMLCite \textit{F. Wolter} and \textit{M. Zakharyaschev}, ACM Trans. Comput. Log. 9, No. 4, Article No. 25, 20 p. (2008; Zbl 1367.03026) Full Text: DOI arXiv
Ghilardi, Silvio; Nicolini, Enrica; Zucchelli, Daniele A comprehensive combination framework. (English) Zbl 1407.03011 ACM Trans. Comput. Log. 9, No. 2, Article No. 8, 54 p. (2008). MSC: 03B35 03B25 03B45 03B15 68T27 PDFBibTeX XMLCite \textit{S. Ghilardi} et al., ACM Trans. Comput. Log. 9, No. 2, Article No. 8, 54 p. (2008; Zbl 1407.03011) Full Text: DOI
Schmidt, Renate A.; Hustadt, Ullrich The axiomatic translation principle for modal logic. (English) Zbl 1367.03045 ACM Trans. Comput. Log. 8, No. 4, Article No. 19, 55 p. (2007). MSC: 03B45 03B25 03B35 68T15 PDFBibTeX XMLCite \textit{R. A. Schmidt} and \textit{U. Hustadt}, ACM Trans. Comput. Log. 8, No. 4, Article No. 19, 55 p. (2007; Zbl 1367.03045) Full Text: DOI
Dovier, Agostino; Formisano, Andrea; Omodeo, Eugenio G. Decidability results for sets with atoms. (English) Zbl 1407.03008 ACM Trans. Comput. Log. 7, No. 2, 269-301 (2006). MSC: 03B25 03B35 03E75 PDFBibTeX XMLCite \textit{A. Dovier} et al., ACM Trans. Comput. Log. 7, No. 2, 269--301 (2006; Zbl 1407.03008) Full Text: DOI
Boigelot, Bernard; Jodogne, Sébastien; Wolper, Pierre An effective decision procedure for linear arithmetic over the integers and reals. (English) Zbl 1407.03052 ACM Trans. Comput. Log. 6, No. 3, 614-633 (2005). MSC: 03D05 03F30 03B25 68Q45 PDFBibTeX XMLCite \textit{B. Boigelot} et al., ACM Trans. Comput. Log. 6, No. 3, 614--633 (2005; Zbl 1407.03052) Full Text: DOI Link
Neven, Frank; Schwentick, Thomas; Vianu, Victor Finite state machines for strings over infinite alphabets. (English) Zbl 1367.68175 ACM Trans. Comput. Log. 5, No. 3, 403-435 (2004). MSC: 68Q45 03B25 03D05 PDFBibTeX XMLCite \textit{F. Neven} et al., ACM Trans. Comput. Log. 5, No. 3, 403--435 (2004; Zbl 1367.68175) Full Text: DOI
Dawar, Anuj; Grädel, Erich; Kreutzer, Stephan Inflationary fixed points in modal logic. (English) Zbl 1407.03031 ACM Trans. Comput. Log. 5, No. 2, 282-315 (2004). MSC: 03B45 03B25 03D15 68Q15 PDFBibTeX XMLCite \textit{A. Dawar} et al., ACM Trans. Comput. Log. 5, No. 2, 282--315 (2004; Zbl 1407.03031) Full Text: DOI
Libkin, Leonid Variable independence for first-order definable constraints. (English) Zbl 1365.03024 ACM Trans. Comput. Log. 4, No. 4, 431-451 (2003). MSC: 03B70 03B25 03C07 03C10 68P15 68Q25 PDFBibTeX XMLCite \textit{L. Libkin}, ACM Trans. Comput. Log. 4, No. 4, 431--451 (2003; Zbl 1365.03024) Full Text: DOI
Kutz, Oliver; Wolter, Frank; Sturm, Holger; Suzuki, Nobu-Yuki; Zakharyaschev, Michael Logics of metric spaces. (English) Zbl 1365.68407 ACM Trans. Comput. Log. 4, No. 2, 260-294 (2003). MSC: 68T27 03B20 03B25 03B45 54E35 68T30 PDFBibTeX XMLCite \textit{O. Kutz} et al., ACM Trans. Comput. Log. 4, No. 2, 260--294 (2003; Zbl 1365.68407) Full Text: DOI
Rybina, Tatiana; Voronkov, Andrei A decision procedure for term algebras with queues. (English) Zbl 1171.68557 ACM Trans. Comput. Log. 2, No. 2, 155-181 (2001). MSC: 68Q65 03B25 03C10 68Q60 PDFBibTeX XMLCite \textit{T. Rybina} and \textit{A. Voronkov}, ACM Trans. Comput. Log. 2, No. 2, 155--181 (2001; Zbl 1171.68557) Full Text: DOI