Journal of Automated Reasoning Short Title: J. Autom. Reasoning Publisher: Springer Netherlands, Dordrecht ISSN: 0168-7433; 1573-0670/e Online: https://link.springer.com/journal/10817/volumes-and-issues Comments: Journal; Indexed cover-to-cover Documents Indexed: 1,141 Publications (since 1985) References Indexed: 800 Publications with 27,937 References. all top 5 Latest Issues 67, No. 3 (2023) 67, No. 2 (2023) 67, No. 1 (2023) 66, No. 4 (2022) 66, No. 3 (2022) 66, No. 2 (2022) 66, No. 1 (2022) 65, No. 8 (2021) 65, No. 7 (2021) 65, No. 6 (2021) 65, No. 5 (2021) 65, No. 4 (2021) 65, No. 3 (2021) 65, No. 2 (2021) 65, No. 1 (2021) 64, No. 8 (2020) 64, No. 7 (2020) 64, No. 6 (2020) 64, No. 5 (2020) 64, No. 4 (2020) 64, No. 3 (2020) 64, No. 2 (2020) 64, No. 1 (2020) 63, No. 4 (2019) 63, No. 3 (2019) 63, No. 2 (2019) 63, No. 1 (2019) 62, No. 4 (2019) 62, No. 3 (2019) 62, No. 2 (2019) 62, No. 1 (2019) 61, No. 1-4 (2018) 60, No. 4 (2018) 60, No. 3 (2018) 60, No. 2 (2018) 60, No. 1 (2018) 59, No. 4 (2017) 59, No. 3 (2017) 59, No. 2 (2017) 59, No. 1 (2017) 58, No. 4 (2017) 58, No. 3 (2017) 58, No. 2 (2017) 58, No. 1 (2017) 57, No. 4 (2016) 57, No. 3 (2016) 57, No. 2 (2016) 57, No. 1 (2016) 56, No. 4 (2016) 56, No. 3 (2016) 56, No. 2 (2016) 56, No. 1 (2016) 55, No. 4 (2015) 55, No. 3 (2015) 55, No. 2 (2015) 55, No. 1 (2015) 54, No. 4 (2015) 54, No. 3 (2015) 54, No. 2 (2015) 54, No. 1 (2015) 53, No. 4 (2014) 53, No. 3 (2014) 53, No. 2 (2014) 53, No. 1 (2014) 52, No. 4 (2014) 52, No. 3 (2014) 52, No. 2 (2014) 52, No. 1 (2014) 51, No. 4 (2013) 51, No. 3 (2013) 51, No. 2 (2013) 51, No. 1 (2013) 50, No. 4 (2013) 50, No. 3 (2013) 50, No. 2 (2013) 50, No. 1 (2013) 49, No. 4 (2012) 49, No. 3 (2012) 49, No. 2 (2012) 49, No. 1 (2012) 48, No. 4 (2012) 48, No. 3 (2012) 48, No. 2 (2012) 48, No. 1 (2012) 47, No. 4 (2011) 47, No. 3 (2011) 47, No. 2 (2011) 47, No. 1 (2011) 46, No. 3-4 (2011) 46, No. 2 (2011) 46, No. 1 (2011) 45, No. 4 (2010) 45, No. 3 (2010) 45, No. 2 (2010) 45, No. 1 (2010) 44, No. 4 (2010) 44, No. 3 (2010) 44, No. 1-2 (2010) 43, No. 4 (2009) 43, No. 3 (2009) ...and 123 more Volumes all top 5 Authors 38 Wos, Larry 20 Paulson, Lawrence Charles 18 Blanchette, Jasmin Christian 12 Bonacina, Maria Paola 12 Nipkow, Tobias 12 Sutcliffe, Geoff 12 Urban, Josef 11 Bundy, Alan 11 Chou, Shangching 11 Giesl, Jürgen 11 McCune, William W. 11 Peltier, Nicolas 10 Plaisted, David Alan 9 Gao, Xiaoshan 9 Kaliszyk, Cezary 9 Veroff, Robert 8 Kapur, Deepak 8 Kaufmann, Matt 8 Leroy, Xavier 8 Moore, J Strother 8 Norrish, Michael 8 Thiemann, René 7 Cantone, Domenico 7 Hustadt, Ullrich 7 Lammich, Peter 7 Middeldorp, Aart 7 Popescu, Andrei 7 Schneider-Kamp, Peter 7 Weidenbach, Christoph 6 Barrett, Clark W. 6 Baumgartner, Peter 6 Blazy, Sandrine 6 Felty, Amy P. 6 Heule, Marijn J. H. 6 Policriti, Alberto 6 Rusinowitch, Michaël 6 Stickel, Mark E. 6 Tourret, Sophie 6 Walsh, Toby 6 Yahya, Adnan H. 6 Zhang, Hantao 5 Appel, Andrew W. 5 Avigad, Jeremy 5 Ayala-Rincón, Mauricio 5 Baader, Franz 5 Basin, David A. 5 Biere, Armin 5 Cristiá, Maximiliano 5 de Moura, Leonardo 5 Divasón, Jose 5 Dixon, Clare 5 Echenim, Mnacho 5 Fiorino, Guido 5 Ghilardi, Silvio 5 Hähnle, Reiner 5 Henschen, Lawrence J. 5 Horrocks, Ian 5 Janičić, Predrag 5 Kazakov, Yevgeny 5 Kunen, Kenneth 5 Lochbihler, Andreas 5 Lucas, Salvador 5 Miller, Dale Allen 5 Narboux, Julien 5 Narendran, Paliath 5 Ohlbach, Hans Jürgen 5 Pąk, Karol 5 Schmidt, Renate A. 5 Smolka, Gert 5 Subrahmanian, V. S. 5 Tinelli, Cesare 5 Urban, Christian 5 Waldmann, Uwe 5 Yamada, Akihisa 5 Zhang, Jingzhong 4 Andrews, Peter B. 4 Barthe, Gilles 4 Bentkamp, Alexander 4 Bledsoe, Woodrow W. 4 Böhme, Sascha 4 Calvanese, Diego 4 Cialdea Mayer, Marta 4 Delaune, Stéphanie 4 Fitelson, Branden 4 Fontaine, Pascal 4 Gamboa, Ruben A. 4 Giunchiglia, Fausto 4 Klein, Gerwin 4 Kohlhase, Michael 4 Korniłowicz, Artur 4 Kremer, Steve 4 Kröning, Daniel 4 Loveland, Donald W. 4 Lu, James J. 4 Lusk, Ewing L. 4 Maggesi, Marco 4 Martín-Mateos, Francisco-Jesús 4 Melquiond, Guillaume 4 Minker, Jack 4 Motik, Boris ...and 1,456 more Authors all top 5 Fields 1,060 Computer science (68-XX) 448 Mathematical logic and foundations (03-XX) 39 General and overarching topics; collections (00-XX) 29 Information and communication theory, circuits (94-XX) 19 Group theory and generalizations (20-XX) 18 Number theory (11-XX) 17 Geometry (51-XX) 15 Operations research, mathematical programming (90-XX) 13 Numerical analysis (65-XX) 10 Order, lattices, ordered algebraic structures (06-XX) 10 Commutative algebra (13-XX) 9 History and biography (01-XX) 9 Combinatorics (05-XX) 9 Category theory; homological algebra (18-XX) 6 Algebraic topology (55-XX) 4 Field theory and polynomials (12-XX) 4 Linear and multilinear algebra; matrix theory (15-XX) 4 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Algebraic geometry (14-XX) 3 Nonassociative rings and algebras (17-XX) 3 Real functions (26-XX) 3 Ordinary differential equations (34-XX) 3 Convex and discrete geometry (52-XX) 3 Differential geometry (53-XX) 3 Probability theory and stochastic processes (60-XX) 3 Quantum theory (81-XX) 3 Relativity and gravitational theory (83-XX) 3 Systems theory; control (93-XX) 2 Associative rings and algebras (16-XX) 2 Functions of a complex variable (30-XX) 2 Several complex variables and analytic spaces (32-XX) 2 Special functions (33-XX) 2 Dynamical systems and ergodic theory (37-XX) 2 General topology (54-XX) 1 Measure and integration (28-XX) 1 Partial differential equations (35-XX) 1 Approximations and expansions (41-XX) 1 Mechanics of particles and systems (70-XX) 1 Biology and other natural sciences (92-XX) 1 Mathematics education (97-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 830 Publications have been cited 7,020 times in 4,037 Documents Cited by ▼ Year ▼ Tractable reasoning and efficient query answering in description logics: The DL-Lite family. Zbl 1132.68725Calvanese, Diego; De Giacomo, Giuseppe; Lembo, Domenico; Lenzerini, Maurizio; Rosati, Riccardo 119 2007 The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0. Zbl 1185.68636Sutcliffe, Geoff 107 2009 The role of the Mizar mathematical library for interactive proof development in Mizar. Zbl 1433.68530Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol 83 2018 The TPTP problem library. CNF release v1. 2. 1. Zbl 0910.68197Sutcliffe, Geoff; Suttner, Christian 69 1998 Basic principles of mechanical theorem proving in elementary geometries. Zbl 0642.68163Wu, Wentsun 68 1986 Four decades of {Mizar}. Foreword. Zbl 1336.00111 66 2015 Theorem proving modulo. Zbl 1049.03011Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude 62 2003 Mechanizing and improving dependency pairs. Zbl 1113.68088Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan 61 2006 Nominal techniques in Isabelle/HOL. Zbl 1140.68061Urban, Christian 58 2008 The foundation of a generic theorem prover. Zbl 0679.68173Paulson, Lawrence C. 58 1989 Algorithms for computing minimal unsatisfiable subsets of constraints. Zbl 1154.68510Liffiton, Mark H.; Sakallah, Karem A. 57 2008 Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Zbl 0967.68145Gomes, Carla P.; Selman, Bart; Crato, Nuno; Kautz, Henry 57 2000 Matrix interpretations for proving termination of term rewriting. Zbl 1139.68049Endrullis, Jörg; Waldmann, Johannes; Zantema, Hans 52 2008 SETHEO: A high-performance theorem prover. Zbl 0759.68080Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W. 50 1992 A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Zbl 0662.68104Stickel, Mark E. 49 1988 Differential dynamic logic for hybrid systems. Zbl 1181.03035Platzer, André 49 2008 Automated deduction by theory resolution. Zbl 0616.68076Stickel, Mark E. 48 1985 Solution of the Robbins problem. Zbl 0883.06011McCune, William 47 1997 Answer set programming based on propositional satisfiability. Zbl 1107.68029Giunchiglia, Enrico; Lierler, Yuliya; Maratea, Marco 44 2006 MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095Urban, Josef 44 2006 The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. Zbl 1425.68381Sutcliffe, Geoff 44 2017 Inferring from inconsistency in preference-based argumentation frameworks. Zbl 1056.68589Amgoud, Leila; Cayrol, Claudette 40 2002 The HOL Light theory of Euclidean space. Zbl 1260.68373Harrison, John 40 2013 A tableau decision procedure for \(\mathcal{SHOIQ}\). Zbl 1132.68734Horrocks, Ian; Sattler, Ulrike 40 2007 Seventy-five problems for testing automatic theorem provers. Zbl 0642.68147Pelletier, Francis Jeffry 38 1986 Extending Sledgehammer with SMT solvers. Zbl 1314.68272Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 37 2013 Translating higher-order clauses to first-order clauses. Zbl 1203.68188Meng, Jia; Paulson, Lawrence C. 36 2008 Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef 36 2014 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283Kaliszyk, Cezary; Urban, Josef 35 2014 Locales: a module system for mathematical theories. Zbl 1315.68218Ballarin, Clemens 35 2014 Controlled integration of the cut rule into connection tableau calculi. Zbl 0816.03005Letz, R.; Mayr, K.; Goller, C. 34 1994 ATP and presentation service for Mizar formalizations. Zbl 1260.68380Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff 34 2013 MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206Akbarpour, Behzad; Paulson, Lawrence Charles 34 2010 MizAR 40 for Mizar 40. Zbl 1356.68191Kaliszyk, Cezary; Urban, Josef 34 2015 Productive use of failure in inductive proof. Zbl 0847.68103Ireland, Andrew; Bundy, Alan 33 1996 IMPS: An interactive mathematical proof system. Zbl 0802.68129Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier 32 1993 Automatic discovery of theorems in elementary geometry. Zbl 0941.03010Recio, T.; Vélez, M. P. 32 1999 A formally verified compiler back-end. Zbl 1185.68215Leroy, Xavier 31 2009 Using typed lambda calculus to implement formal systems on a machine. Zbl 0784.68072Avron, Arnon; Honsell, Furio; Mason, Ian A.; Pollack, Robert 30 1992 Model-theoretic methods in combined constraint satisfiability. Zbl 1069.03008Ghilardi, Silvio 30 2004 Explicit representation of terms defined by counter examples. Zbl 0641.68124Lassez, J.-L.; Marriott, K. 29 1987 Eliminating dublication with the hyper-linking strategy. Zbl 0784.68077Lee, Shie-Jue; Plaisted, David A. 29 1992 Set theory for verification. I: From foundations to functions. Zbl 0802.68128Paulson, Lawrence C. 29 1993 lean\(T^ AP\): Lean tableau-based deduction. Zbl 0838.68097Beckert, Bernhard; Posegga, Joachim 28 1995 Experiments with discrimination-tree indexing and path indexing for term retrieval. Zbl 0781.68101McCune, William 27 1992 Deduction in non-Horn databases. Zbl 0614.68072Yahya, Adnan; Henschen, Lawrence J. 27 1985 An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. Zbl 1002.68165Cadoli, Marco; Schaerf, Marco; Giovanardi, Andrea; Giovanardi, Massimo 27 2002 A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142Harrison, J.; Théry, L. 26 1998 Stochastic Boolean satisfiability. Zbl 0988.68189Littman, Michael L.; Majercik, Stephen M.; Pitassi, Toniann 26 2001 Backdoor sets of quantified Boolean formulas. Zbl 1191.68353Samer, Marko; Szeider, Stefan 26 2009 Logical cryptanalysis as a SAT problem: Encoding and analysis of the U. S. Data Encryption Standard. Zbl 0968.68052Massacci, Fabio; Marraro, Laura 26 2000 Non-Horn clause logic programming without contrapositives. Zbl 0666.68091Plaisted, David A. 25 1988 Computing circumscription revisited: A reduction algorithm. Zbl 0939.03033Doherty, Patrick; Łukaszewicz, Witold; Szałas, Andrzej 25 1997 Some lambda calculus and type theory formalized. Zbl 0940.03019McKinna, James; Pollack, Robert 25 1999 Complexity of unification problems with associative-commutative operators. Zbl 0781.68076Kapur, Deepak; Narendran, Paliath 24 1992 Ordered semantic hyper-linking. Zbl 0959.68115Plaisted, David A.; Zhu, Yunshan 24 2000 Mechanically proving termination using polynomial interpretations. Zbl 1108.03017Contejean, Evelyne; Marché, Claude; Tomás, Ana Paula; Urbain, Xavier 23 2005 Implicit induction in conditional theories. Zbl 0819.68114Bouhoula, Adel; Rusinowitch, Michaël 23 1995 The locally nameless representation. Zbl 1260.68368Charguéraud, Arthur 23 2012 MPTP-motivation, implementation, first experiments. Zbl 1075.68081Urban, Josef 23 2004 Branching rules for satisfiability. Zbl 0838.68098Hooker, J. N.; Vinay, V. 22 1995 Testing positiveness of polynomials. Zbl 0916.68084Hong, Hoon; Jakuš, Dalibor 22 1998 Using hints to increase the effectiveness of an automated reasoning program: Case studies. Zbl 0857.68095Veroff, Robert 22 1996 Closed-form upper bounds in static cost analysis. Zbl 1213.68200Albert, Elvira; Arenas, Puri; Genaim, Samir; Puebla, Germán 22 2011 A graphical user interface for formal proofs in geometry. Zbl 1131.68094Narboux, Julien 22 2007 Mechanized semantics for the clight subset of the C language. Zbl 1185.68136Blazy, Sandrine; Leroy, Xavier 22 2009 The ILTP problem library for intuitionistic logic. Zbl 1113.68093Raths, Thomas; Otten, Jens; Kreitz, Christoph 22 2007 Analyzing program termination and complexity automatically with AProVE. Zbl 1409.68255Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René 22 2017 First-order modal tableaux. Zbl 0648.03004Fitting, Melvin 21 1988 A logic for reasoning with inconsistency. Zbl 0807.03019Kifer, Michael; Lozinskii, Eliezer L. 21 1992 Combining nonstably infinite theories. Zbl 1108.03014Tinelli, Cesare; Zarba, Calogero G. 21 2005 From bisimulation to simulation: Coarsest partition problems. Zbl 1081.68052Gentilini, R.; Piazza, C.; Policriti, A. 21 2003 New worst-case upper bounds for SAT. Zbl 0960.03009Hirsch, Edward A. 21 2000 Unification in abelian semigroups. Zbl 0637.68106Herold, Alexander; Siekmann, Jörg H. 20 1987 On the declarative and procedural semantics of logic programs. Zbl 0681.68109Przymusinski, Teodor C. 20 1989 The area method. A recapitulation. Zbl 1242.68281Janičić, Predrag; Narboux, Julien; Quaresma, Pedro 20 2012 On deciding satisfiability by theorem proving with speculative inferences. Zbl 1243.68265Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo 20 2011 Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. Zbl 1252.68252Felty, Amy; Momigliano, Alberto 20 2012 A two-level logic approach to reasoning about computations. Zbl 1290.68088Gacek, Andrew; Miller, Dale; Nadathur, Gopalan 20 2012 Automated theorem proving in GeoGebra: current achievements. Zbl 1356.68181Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon 20 2015 Local search algorithms for SAT: an empirical evaluation. Zbl 0961.68039Hoos, Holger H.; Stützle, Thomas 20 2000 Hammer for Coq: automation for dependent type theory. Zbl 1448.68458Czajka, Łukasz; Kaliszyk, Cezary 20 2018 Gentzen-type systems, resolution and tableaux. Zbl 0788.03013Avron, Arnon 19 1993 Priorities on defaults with prerequisites, and their application in treating specificity in terminological default logic. Zbl 0842.68081Baader, Franz; Hollunder, Bernhard 19 1995 Short single axioms for Boolean algebra. Zbl 1014.06012McCune, William; Veroff, Robert; Fitelson, Branden; Harris, Kenneth; Feist, Andrew; Wos, Larry 19 2002 Autarkic computations in formal proofs. Zbl 1002.68156Barendregt, Henk; Barendsen, Erik 19 2002 TPS: A theorem-proving system for classical type theory. Zbl 0858.03017Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei 19 1996 Complexity and resource bound analysis of imperative programs using difference constraints. Zbl 1409.68076Sinn, Moritz; Zuleger, Florian; Veith, Helmut 19 2017 The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies. Zbl 1331.68216Kazakov, Yevgeny; Krötzsch, Markus; Simančík, František 19 2014 A deductive database approach to automated geometry theorem proving and discovering. Zbl 0961.68121Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong 19 2000 The theory of idempotent semigroups is of unification type zero. Zbl 0626.68070Baader, Franz 18 1986 Set theory in first-order logic: Clauses for Gödel’s axioms. Zbl 0635.03008Boyer, Robert; Lusk, Ewing; McCune, William; Overbeek, Ross; Stickel, Mark E.; Wos, Lawrence 18 1986 Dualities between alternative semantics for logic programming and nonmonotonic reasoning. Zbl 0782.68074Baral, Chitta R.; Subrahmanian, V. S. 18 1993 A semantical framework for supporting subjective and conditional probabilities in deductive databases. Zbl 0784.68082Ng, Raymond; Subrahmanian, V. S. 18 1993 Conjecture synthesis for inductive theories. Zbl 1243.68268Johansson, Moa; Dixon, Lucas; Bundy, Alan 18 2011 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 18 2013 Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Zbl 1267.68208Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre 18 2013 Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090Krauss, Alexander; Nipkow, Tobias 18 2012 Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Zbl 1109.68098Alekhnovich, Michael; Hirsch, Edward A.; Itsykson, Dmitry 18 2005 Reachability analysis over term rewriting systems. Zbl 1075.68038Feuillade, Guillaume; Genet, Thomas; Viet Triem Tong, Valérie 18 2004 Rensets and renaming-based recursion for syntax with bindings extended version. Zbl 07722430Popescu, Andrei 1 2023 Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL. Zbl 07498610Dalvandi, Sadegh; Dongol, Brijesh; Doherty, Simon; Wehrheim, Heike 2 2022 Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs. Zbl 07498608Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan 1 2022 Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL. Zbl 07498609Huerta y Munive, Jonathan Julián; Struth, Georg 1 2022 A Coq formalization of Lebesgue integration of nonnegative functions. Zbl 07538894Boldo, Sylvie; Clément, François; Faissole, Florian; Martin, Vincent; Mayero, Micaela 1 2022 Larry Wos: visions of automated reasoning. Zbl 1511.68005Beeson, Michael; Bonacina, Maria Paola; Kinyon, Michael; Sutcliffe, Geoff 1 2022 A Wos challenge met. Zbl 1512.68430Veroff, Robert 1 2022 Local is best: efficient reductions to modal logic K. Zbl 1512.68425Papacchini, Fabio; Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare 1 2022 Verifying Whiley programs with Boogie. Zbl 1512.68059Pearce, David J.; Utting, Mark; Groves, Lindsay 1 2022 Towards formalising Schutz’ axioms for Minkowski spacetime in Isabelle/HOL. Zbl 1511.68331Schmoetten, Richard; Palmer, Jake E.; Fleuriot, Jacques D. 1 2022 TacticToe: learning to prove with tactics. Zbl 07356973Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael 6 2021 Extensional higher-order paramodulation in Leo-III. Zbl 1509.68321Steen, Alexander; Benzmüller, Christoph 5 2021 Superposition with lambdas. Zbl 07433023Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe 5 2021 Automated proof of Bell-LaPadula security properties. Zbl 07356979Cristiá, Maximiliano; Rossi, Gianfranco 5 2021 Automated reasoning with restricted intensional sets. Zbl 07432188Cristiá, Maximiliano; Rossi, Gianfranco 3 2021 Building strategies into QBF proofs. Zbl 07356969Beyersdorff, Olaf; Blinkhorn, Joshua; Mahajan, Meena 3 2021 Machine learning guidance for connection tableaux. Zbl 07356974Färber, Michael; Kaliszyk, Cezary; Urban, Josef 3 2021 On the importance of domain model configuration for automated planning engines. Zbl 07432186Vallati, Mauro; Chrpa, Lukáš; McCluskey, Thomas Leo; Hutter, Frank 2 2021 Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes). Zbl 07433024Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey 2 2021 An automatically verified prototype of the Tokeneer ID station specification. Zbl 07461267Cristiá, Maximiliano; Rossi, Gianfranco 2 2021 Optimization modulo the theories of signed bit-vectors and floating-point numbers. Zbl 07433028Trentin, Patrick; Sebastiani, Roberto 1 2021 Formalization of Euler-Lagrange equation set based on variational calculus in HOL light. Zbl 07356966Guan, Yong; Zhang, Jingzhi; Wang, Guohui; Li, Ximeng; Shi, Zhiping; Li, Yongdong 1 2021 Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 07356971Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 1 2021 Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates. Zbl 07356976Voigt, Marco 1 2021 Higher-order quantifier elimination, counter simulations and fault-tolerant systems. Zbl 07356977Ghilardi, Silvio; Pagani, Elena 1 2021 Human-centered automated proof search. Zbl 07461268Sieg, Wilfried; Derakhshan, Farzaneh 1 2021 Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem. Zbl 1493.68389de Lima, Thaynara Arielly; Galdino, André Luiz; Avelar, Andréia Borges; Ayala-Rincón, Mauricio 1 2021 Experiences from exporting major proof assistant libraries. Zbl 07461271Kohlhase, Michael; Rabe, Florian 1 2021 A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 1469.68165Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 8 2020 Strong extension-free proof systems. Zbl 1468.03011Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin 7 2020 Solving quantifier-free first-order constraints over finite sets and binary relations. Zbl 1468.03009Cristiá, Maximiliano; Rossi, Gianfranco 6 2020 OptiMathSAT: a tool for optimization modulo theories. Zbl 1468.68206Sebastiani, Roberto; Trentin, Patrick 6 2020 Conflict-driven satisfiability for theory combination: transition system and completeness. Zbl 1468.68194Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan 6 2020 Scalable fine-grained proofs for formula processing. Zbl 1468.68278Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal 5 2020 The MetaCoq project. Zbl 1468.68075Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo 5 2020 Exploring the structure of an algebra text with locales. Zbl 1468.68277Ballarin, Clemens 5 2020 System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David 4 2020 Politeness and combination methods for theories with bridging functions. Zbl 1468.68143Chocron, Paula; Fontaine, Pascal; Ringeissen, Christophe 4 2020 Blocking and other enhancements for bottom-up model generation methods. Zbl 1468.68279Baumgartner, Peter; Schmidt, Renate A. 4 2020 \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments. Zbl 1468.68304Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare 4 2020 Efficient verified (UN)SAT certificate checking. Zbl 1468.68134Lammich, Peter 4 2020 Automatically verifying temporal properties of pointer programs with cyclic proof. Zbl 1468.68137Tellez, Gadi; Brotherston, James 4 2020 A formalized general theory of syntax with bindings: extended version. Zbl 1468.68073Gheri, Lorenzo; Popescu, Andrei 4 2020 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe 4 2020 ICE-based refinement type discovery for higher-order functional programs. Zbl 1468.68059Champion, Adrien; Chiba, Tomoya; Kobayashi, Naoki; Sato, Ryosuke 4 2020 The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques. Zbl 1459.68092Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl 3 2020 Loop-type sequent calculi for temporal logic. Zbl 1462.03012Alonderis, R.; Pliuškevičius, R.; Pliuškevičienė, A.; Giedra, H. 3 2020 Using well-founded relations for proving operational termination. Zbl 1468.03034Lucas, Salvador 3 2020 Combining induction and saturation-based theorem proving. Zbl 1476.68300Echenim, M.; Peltier, N. 3 2020 Probably partially true: satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. Zbl 1468.68200Finger, Marcelo; Preto, Sandro 3 2020 Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL. Zbl 1468.68299Li, Wenda; Paulson, Lawrence C. 2 2020 A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 1468.68326Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 2 2020 Verified analysis of random binary tree structures. Zbl 1468.68289Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 2 2020 First-order automated reasoning with theories: when deduction modulo theory meets practice. Zbl 1468.68282Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier 2 2020 Multi-cost bounded tradeoff analysis in MDP. Zbl 1468.68132Hartmanns, Arnd; Junges, Sebastian; Katoen, Joost-Pieter; Quatmann, Tim 2 2020 Theorem proving for pointwise metric temporal logic over the naturals via translations. Zbl 1459.03012Hustadt, Ullrich; Ozaki, Ana; Dixon, Clare 1 2020 Automating free logic in HOL, with an experimental application in category theory. Zbl 1434.68639Benzmüller, Christoph; Scott, Dana S. 1 2020 Limited second-order functionality in a first-order setting. Zbl 1468.68291Kaufmann, Matt; Moore, J Strother 1 2020 Graph theory in Coq: minors, treewidth, and isomorphisms. Zbl 1468.68320Doczkal, Christian; Pous, Damien 1 2020 A library for formalization of linear error-correcting codes. Zbl 1468.68314Affeldt, Reynald; Garrigue, Jacques; Saikawa, Takafumi 1 2020 Constructive decision via redundancy-free proof-search. Zbl 1468.03015Larchey-Wendling, Dominique 1 2020 Simulating strong practical proof systems with extended resolution. Zbl 1468.68293Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.; Biere, Armin 1 2020 Parameterized model checking on the TSO weak memory model. Zbl 1468.68123Conchon, Sylvain; Declerck, David; Zaïdi, Fatiha 1 2020 Fine-grained complexity of safety verification. Zbl 1468.68121Chini, Peter; Meyer, Roland; Saivasan, Prakash 1 2020 A learning-based approach to synthesizing invariants for incomplete verification engines. Zbl 1468.68074Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun 1 2020 Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Zbl 1468.68120Charguéraud, Arthur; Pottier, François 10 2019 From types to sets by local type definition in higher-order logic. Zbl 1468.68295Kunčar, Ondřej; Popescu, Andrei 8 2019 Refinement to imperative HOL. Zbl 1465.68291Lammich, Peter 8 2019 Canonicity for cubical type theory. Zbl 1477.03036Huber, Simon 8 2019 Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Zbl 1441.03011Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal 7 2019 A consistent foundation for Isabelle/HOL. Zbl 1465.68289Kunčar, Ondřej; Popescu, Andrei 7 2019 Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 1468.68328Lammich, Peter; Sefidgar, S. Reza 6 2019 The univalence axiom in cubical sets. Zbl 1506.03064Bezem, Marc; Coquand, Thierry; Huber, Simon 6 2019 Semantics of Mizar as an Isabelle object logic. Zbl 1468.68290Kaliszyk, Cezary; Pąk, Karol 5 2019 Verifying OpenJDK’s sort method for generic collections. Zbl 1468.68125de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic 4 2019 Guarded cubical type theory. Zbl 1477.03034Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea 4 2019 The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory. Zbl 1477.03035Brunerie, Guillaume 4 2019 A proof theory for model checking. Zbl 1468.03078Heath, Quentin; Miller, Dale 4 2019 The flow of ODEs: formalization of variational equation and Poincaré map. Zbl 1468.68325Immler, Fabian; Traut, Christoph 3 2019 Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. Zbl 1468.68302Marić, Filip 3 2019 Amortized complexity verified. Zbl 1465.68060Nipkow, Tobias; Brinkop, Hauke 3 2019 A formalization of convex polyhedra based on the simplex method. Zbl 1468.68316Allamigeon, Xavier; Katz, Ricardo D. 3 2019 Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. Zbl 1468.03008Beyersdorff, Olaf; Blinkhorn, Joshua; Chew, Leroy; Schmidt, Renate; Suda, Martin 3 2019 Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 1468.68318Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter 3 2019 Formalization of metatheory of the Quipper quantum programming language in a linear logic. Zbl 1468.68330Mahmoud, Mohamed Yousri; Felty, Amy P. 3 2019 Compositional falsification of cyber-physical systems with machine learning components. Zbl 1468.68126Dreossi, Tommaso; Donzé, Alexandre; Seshia, Sanjit A. 3 2019 Efficient active automata learning via mutation testing. Zbl 1468.68117Aichernig, Bernhard K.; Tappler, Martin 3 2019 System-level non-interference of constant-time cryptography. I: Model. Zbl 1459.68026Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos 3 2019 Formally verified approximations of definite integrals. Zbl 1468.68301Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas 2 2019 Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Zbl 1468.68298Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C. 2 2019 A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data. Zbl 1465.68041Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre 2 2019 From signatures to monads in UniMath. Zbl 1468.03007Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders 2 2019 Call-by-value lambda calculus as a model of computation in Coq. Zbl 1468.68323Forster, Yannick; Smolka, Gert 2 2019 Categoricity results and large model constructions for second-order ZF in dependent type theory. Zbl 1468.03013Kirst, Dominik; Smolka, Gert 2 2019 Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68062Lochbihler, Andreas 2 2019 Formalization of geometric algebra in HOL Light. Zbl 1468.68329Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong 2 2019 QPCF: higher-order languages and quantum circuits. Zbl 1468.68049Paolini, Luca; Piccolo, Mauro; Zorzi, Margherita 2 2019 Explaining AI decisions using efficient methods for learning sparse Boolean formulae. Zbl 1468.68149Jha, Susmit; Sahai, Tuhin; Raman, Vasumathi; Pinto, Alessandro; Francis, Michael 2 2019 An automata-theoretic approach to model-checking systems and specifications over infinite data domains. Zbl 1468.68128Frenkel, Hadar; Grumberg, Orna; Sheinvald, Sarai 2 2019 Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228Lammich, Peter; Lochbihler, Andreas 2 2019 ...and 730 more Documents all cited Publications top 5 cited Publications all top 5 Cited by 4,524 Authors 43 Urban, Josef 42 Paulson, Lawrence Charles 32 Kaliszyk, Cezary 29 Blanchette, Jasmin Christian 29 Eiter, Thomas 28 Meseguer Guaita, José 27 Weidenbach, Christoph 26 Baader, Franz 26 Benzmüller, Christoph Ewald 26 Lucas, Salvador 25 Middeldorp, Aart 24 Grabowski, Adam 23 Giesl, Jürgen 22 Gao, Xiaoshan 22 Marques-Silva, João P. 20 Bonacina, Maria Paola 20 Nipkow, Tobias 20 Platzer, André 20 Voronkov, Andrei 19 Ghilardi, Silvio 19 Korniłowicz, Artur 19 Subramani, Krishnan 19 Sutcliffe, Geoff 19 Thiemann, René 19 Tinelli, Cesare 18 Ayala-Rincón, Mauricio 18 Kapur, Deepak 18 Peltier, Nicolas 18 Rabe, Florian 17 Waldmann, Uwe 16 Biere, Armin 16 Calvanese, Diego 16 Gottlob, Georg 16 Heule, Marijn J. H. 16 Koch, Sebastian 16 Pąk, Karol 16 Schaub, Torsten H. 16 Schneider-Kamp, Peter 15 Bundy, Alan 15 Cantone, Domenico 15 Janičić, Predrag 15 Moser, Georg 14 Barrett, Clark W. 14 Baumgartner, Peter 14 Kohlhase, Michael 14 Nakasho, Kazuhisa 14 Smolka, Gert 14 Szeider, Stefan 14 Wos, Larry 13 Dixon, Clare 13 Dowek, Gilles 13 Narboux, Julien 13 Naumowicz, Adam 13 Plaisted, David Alan 13 Reger, Giles 13 Reynolds, Andrew 13 Ringeissen, Christophe 13 Rusinowitch, Michaël 13 Shidama, Yasunari 13 Subrahmanian, V. S. 13 Tahar, Sofiène 13 Wang, Dongming 13 Winkler, Sarah 12 Alviano, Mario 12 Bonatti, Piero Andrea 12 Chou, Shangching 12 Fernández, Maribel 12 Goré, Rajeev Prabhakar 12 Gutiérrez, Raúl 12 Horrocks, Ian 12 Kirchner, Claude 12 Kutsia, Temur 12 Miller, Dale Allen 12 Nigam, Vivek 12 Pientka, Brigitte 12 Popescu, Andrei 12 Schmidt-Schauß, Manfred 12 Schwarzweller, Christoph 12 Struth, Georg 12 Tourret, Sophie 12 Zakharyaschev, Michael Viktorovich 12 Zhang, Hantao 11 Amgoud, Leila 11 Botana, Francisco 11 Brown, Chad Edward 11 Felty, Amy P. 11 Gabbay, Dov M. 11 Giunchiglia, Enrico 11 Kovács, Zoltán 11 Kuncak, Viktor 11 Lochbihler, Andreas 11 Maratea, Marco 11 Montanari, Angelo 11 Otten, Jens 11 Pimentel, Elaine 11 Recio, Tomas 11 Sebastiani, Roberto 11 Sternagel, Christian 11 Wolter, Frank 11 Zankl, Harald ...and 4,424 more Authors all top 5 Cited in 236 Journals 508 Journal of Automated Reasoning 209 Artificial Intelligence 186 Theoretical Computer Science 126 Journal of Symbolic Computation 123 Annals of Mathematics and Artificial Intelligence 109 Formalized Mathematics 78 Information and Computation 61 Theory and Practice of Logic Programming 56 MSCS. Mathematical Structures in Computer Science 48 Logical Methods in Computer Science 47 Formal Aspects of Computing 45 International Journal of Approximate Reasoning 43 Journal of Applied Logic 39 Journal of Applied Non-Classical Logics 39 Journal of Logical and Algebraic Methods in Programming 35 Annals of Pure and Applied Logic 32 Discrete Applied Mathematics 32 Formal Methods in System Design 30 Journal of Functional Programming 26 Constraints 26 Mathematics in Computer Science 25 Information Processing Letters 22 Information Sciences 22 Journal of Computer and System Sciences 21 Studia Logica 20 Fuzzy Sets and Systems 20 ACM Transactions on Computational Logic 18 Applied Mathematics and Computation 16 Acta Informatica 15 Computers & Mathematics with Applications 14 Applicable Algebra in Engineering, Communication and Computing 14 Journal of Systems Science and Complexity 13 New Generation Computing 12 The Journal of Symbolic Logic 12 Logica Universalis 11 AI Communications 11 Fundamenta Informaticae 11 The Journal of Logic and Algebraic Programming 10 Journal of Computer Science and Technology 10 The Journal of Artificial Intelligence Research (JAIR) 8 Synthese 8 Science of Computer Programming 8 International Journal of Computer Mathematics 8 Journal of Logic, Language and Information 8 The Bulletin of Symbolic Logic 8 Soft Computing 7 Automatica 7 Journal of Philosophical Logic 7 Notre Dame Journal of Formal Logic 7 JETAI. Journal of Experimental & Theoretical Artificial Intelligence 7 Computational Geometry 6 International Journal of General Systems 6 Mathematics and Computers in Simulation 6 Computers & Operations Research 6 European Journal of Operational Research 6 Computer Languages, Systems & Structures 6 Journal of Satisfiability, Boolean Modeling and Computation 6 The Review of Symbolic Logic 5 International Journal of Intelligent Systems 5 Annals of Operations Research 5 Archive for Mathematical Logic 5 Theory of Computing Systems 5 Higher-Order and Symbolic Computation 5 Journal of Formalized Reasoning 5 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 5 Prikladnaya Diskretnaya Matematika 4 Communications in Algebra 4 Algorithmica 4 Mathematical and Computer Modelling 4 Machine Learning 4 International Journal of Foundations of Computer Science 4 Indagationes Mathematicae. New Series 4 Computational Complexity 4 Journal of Mathematical Sciences (New York) 4 Journal of Combinatorial Optimization 4 LMS Journal of Computation and Mathematics 4 Journal of Applied Mathematics 4 Nonlinear Analysis. Hybrid Systems 4 Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas. RACSAM 3 Journal of Algebra 3 Semigroup Forum 3 Science in China. Series A 3 Experimental Mathematics 3 Mathematical Logic Quarterly (MLQ) 3 Journal of Heuristics 3 Mathematical Problems in Engineering 3 Communications in Nonlinear Science and Numerical Simulation 3 International Journal of Applied Mathematics and Computer Science 3 RAIRO. Theoretical Informatics and Applications 3 Journal of Discrete Algorithms 3 Lietuvos Matematikos Rinkinys. Proceedings of the Lithuanian Mathematical Society. Series A 2 Discrete Mathematics 2 Journal of Mathematical Physics 2 Mathematics of Computation 2 The Mathematical Intelligencer 2 Computing 2 Journal of Computational and Applied Mathematics 2 Journal of Mathematical Economics 2 Journal of Pure and Applied Algebra 2 Programming and Computer Software ...and 136 more Journals all top 5 Cited in 53 Fields 3,449 Computer science (68-XX) 1,415 Mathematical logic and foundations (03-XX) 122 Operations research, mathematical programming (90-XX) 103 Information and communication theory, circuits (94-XX) 72 Numerical analysis (65-XX) 71 Geometry (51-XX) 63 Combinatorics (05-XX) 54 Order, lattices, ordered algebraic structures (06-XX) 53 Commutative algebra (13-XX) 49 Number theory (11-XX) 43 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 42 Group theory and generalizations (20-XX) 42 Systems theory; control (93-XX) 33 Field theory and polynomials (12-XX) 33 Category theory; homological algebra (18-XX) 30 Algebraic geometry (14-XX) 26 General and overarching topics; collections (00-XX) 26 Real functions (26-XX) 25 History and biography (01-XX) 24 General algebraic systems (08-XX) 20 Ordinary differential equations (34-XX) 18 Algebraic topology (55-XX) 17 Biology and other natural sciences (92-XX) 14 Linear and multilinear algebra; matrix theory (15-XX) 14 Probability theory and stochastic processes (60-XX) 13 Statistics (62-XX) 12 Quantum theory (81-XX) 11 Associative rings and algebras (16-XX) 11 Mathematics education (97-XX) 9 Partial differential equations (35-XX) 9 Dynamical systems and ergodic theory (37-XX) 9 Operator theory (47-XX) 8 Mechanics of particles and systems (70-XX) 7 Measure and integration (28-XX) 7 Special functions (33-XX) 7 Functional analysis (46-XX) 7 Convex and discrete geometry (52-XX) 5 Calculus of variations and optimal control; optimization (49-XX) 4 Nonassociative rings and algebras (17-XX) 4 Optics, electromagnetic theory (78-XX) 4 Relativity and gravitational theory (83-XX) 3 Functions of a complex variable (30-XX) 3 Sequences, series, summability (40-XX) 3 Approximations and expansions (41-XX) 3 Harmonic analysis on Euclidean spaces (42-XX) 3 Differential geometry (53-XX) 3 General topology (54-XX) 2 Difference and functional equations (39-XX) 2 Integral equations (45-XX) 2 Fluid mechanics (76-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Mechanics of deformable solids (74-XX) 1 Geophysics (86-XX) Citations by Year