# zbMATH — the first resource for mathematics

## Journal of Automated Reasoning

 Short Title: J. Autom. Reasoning Publisher: Springer Netherlands, Dordrecht ISSN: 0168-7433; 1573-0670/e Online: http://link.springer.com/journal/volumesAndIssues/10817 Comments: Indexed cover-to-cover
 Documents Indexed: 1,055 Publications (since 1985) References Indexed: 719 Publications with 24,011 References.
all top 5

#### Latest Issues

 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) 43, No. 2 (2009) 43, No. 1 (2009) 42, No. 2-4 (2009) 42, No. 1 (2009) 41, No. 3-4 (2008) 41, No. 2 (2008) 41, No. 1 (2008) 40, No. 4 (2008) 40, No. 2-3 (2008) 40, No. 1 (2008) 39, No. 4 (2007) ...and 112 more Volumes
all top 5

#### Authors

 38 Wos, Larry 19 Paulson, Lawrence Charles 13 Blanchette, Jasmin Christian 12 Urban, Josef 11 Bundy, Alan 11 Chou, Shangching 11 Giesl, Jürgen 11 McCune, William W. 11 Nipkow, Tobias 11 Sutcliffe, Geoff 10 Peltier, Nicolas 10 Plaisted, David Alan 9 Gao, Xiaoshan 8 Kaliszyk, Cezary 8 Kaufmann, Matt 8 Moore, J Strother 8 Norrish, Michael 8 Veroff, Robert 7 Bonacina, Maria Paola 7 Cantone, Domenico 7 Kapur, Deepak 7 Lammich, Peter 7 Leroy, Xavier 7 Schneider-Kamp, Peter 6 Baumgartner, Peter 6 Blazy, Sandrine 6 Felty, Amy P. 6 Middeldorp, Aart 6 Policriti, Alberto 6 Rusinowitch, Michaël 6 Stickel, Mark E. 6 Thiemann, René 6 Walsh, Toby 6 Yahya, Adnan H. 6 Zhang, Hantao 5 Avigad, Jeremy 5 Basin, David A. 5 Biere, Armin 5 de Moura, Leonardo 5 Echenim, Mnacho 5 Hähnle, Reiner 5 Henschen, Lawrence J. 5 Horrocks, Ian 5 Hustadt, Ullrich 5 Kazakov, Yevgeny 5 Kunen, Kenneth 5 Miller, Dale Allen 5 Narendran, Paliath 5 Ohlbach, Hans Jürgen 5 Popescu, Andrei 5 Schmidt, Renate A. 5 Smolka, Gert 5 Subrahmanian, V. S. 5 Weidenbach, Christoph 4 Andrews, Peter B. 4 Barthe, Gilles 4 Bledsoe, Woodrow W. 4 Böhme, Sascha 4 Cialdea Mayer, Marta 4 Delaune, Stéphanie 4 Fiorino, Guido 4 Fitelson, Branden 4 Gamboa, Ruben A. 4 Giunchiglia, Fausto 4 Heule, Marijn J. H. 4 Janičić, Predrag 4 Klein, Gerwin 4 Korniłowicz, Artur 4 Kremer, Steve 4 Lochbihler, Andreas 4 Loveland, Donald W. 4 Lu, James J. 4 Lucas, Salvador 4 Lusk, Ewing L. 4 Martín-Mateos, Francisco-Jesús 4 Melquiond, Guillaume 4 Minker, Jack 4 Motik, Boris 4 Muñoz, César A. 4 Murray, Neil V. 4 Myreen, Magnus O. 4 Narboux, Julien 4 Overbeek, Ross A. 4 Pąk, Karol 4 Pelletier, Francis Jeffry 4 Quaife, Art 4 Rudnicki, Piotr 4 Ruiz-Reina, José-Luis 4 Schulz, Stephan 4 Suttner, Christian B. 4 Szeider, Stefan 4 Théry, Laurent 4 Urban, Christian 4 Voronkov, Andrei 4 Yamada, Akihisa 4 Zarba, Calogero G. 4 Zhang, Jingzhong 3 Alonso, José-Antonio 3 Anantharaman, Siva 3 Appel, Andrew W. ...and 1,347 more Authors
all top 5

#### Fields

 973 Computer science (68-XX) 436 Mathematical logic and foundations (03-XX) 36 General and overarching topics; collections (00-XX) 29 Information and communication theory, circuits (94-XX) 18 Group theory and generalizations (20-XX) 16 Number theory (11-XX) 16 Geometry (51-XX) 15 Operations research, mathematical programming (90-XX) 13 Numerical analysis (65-XX) 10 Order, lattices, ordered algebraic structures (06-XX) 7 History and biography (01-XX) 7 Combinatorics (05-XX) 6 Commutative algebra (13-XX) 6 Category theory; homological algebra (18-XX) 4 Field theory and polynomials (12-XX) 4 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Algebraic geometry (14-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 Algebraic topology (55-XX) 3 Systems theory; control (93-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 2 Nonassociative rings and algebras (17-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) 2 Probability theory and stochastic processes (60-XX) 2 Quantum theory (81-XX) 1 Associative rings and algebras (16-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 Relativity and gravitational theory (83-XX) 1 Biology and other natural sciences (92-XX) 1 Mathematics education (97-XX)

#### Citations contained in zbMATH Open

729 Publications have been cited 5,058 times in 3,111 Documents Cited by Year
Tractable reasoning and efficient query answering in description logics: The DL-Lite family. Zbl 1132.68725
Calvanese, Diego; De Giacomo, Giuseppe; Lembo, Domenico; Lenzerini, Maurizio; Rosati, Riccardo
2007
The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0. Zbl 1185.68636
Sutcliffe, Geoff
2009
The TPTP problem library. CNF release v1. 2. 1. Zbl 0910.68197
Sutcliffe, Geoff; Suttner, Christian
1998
Four decades of {Mizar}. Foreword. Zbl 1336.00111
2015
Basic principles of mechanical theorem proving in elementary geometries. Zbl 0642.68163
Wu, Wentsun
1986
Theorem proving modulo. Zbl 1049.03011
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
2003
The role of the Mizar mathematical library for interactive proof development in Mizar. Zbl 1433.68530
Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol
2018
Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Zbl 0967.68145
Gomes, Carla P.; Selman, Bart; Crato, Nuno; Kautz, Henry
2000
Nominal techniques in Isabelle/HOL. Zbl 1140.68061
Urban, Christian
2008
Solution of the Robbins problem. Zbl 0883.06011
McCune, William
1997
The foundation of a generic theorem prover. Zbl 0679.68173
Paulson, Lawrence C.
1989
A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Zbl 0662.68104
Stickel, Mark E.
1988
SETHEO: A high-performance theorem prover. Zbl 0759.68080
Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W.
1992
Automated deduction by theory resolution. Zbl 0616.68076
Stickel, Mark E.
1985
Mechanizing and improving dependency pairs. Zbl 1113.68088
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan
2006
Algorithms for computing minimal unsatisfiable subsets of constraints. Zbl 1154.68510
Liffiton, Mark H.; Sakallah, Karem A.
2008
Matrix interpretations for proving termination of term rewriting. Zbl 1139.68049
Endrullis, Jörg; Waldmann, Johannes; Zantema, Hans
2008
Seventy-five problems for testing automatic theorem provers. Zbl 0642.68147
Pelletier, Francis Jeffry
1986
Answer set programming based on propositional satisfiability. Zbl 1107.68029
Giunchiglia, Enrico; Lierler, Yuliya; Maratea, Marco
2006
A tableau decision procedure for $$\mathcal{SHOIQ}$$. Zbl 1132.68734
Horrocks, Ian; Sattler, Ulrike
2007
Controlled integration of the cut rule into connection tableau calculi. Zbl 0816.03005
Letz, R.; Mayr, K.; Goller, C.
1994
Productive use of failure in inductive proof. Zbl 0847.68103
Ireland, Andrew; Bundy, Alan
1996
Inferring from inconsistency in preference-based argumentation frameworks. Zbl 1056.68589
Amgoud, Leila; Cayrol, Claudette
2002
IMPS: An interactive mathematical proof system. Zbl 0802.68129
Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier
1993
The HOL Light theory of Euclidean space. Zbl 1260.68373
Harrison, John
2013
Using typed lambda calculus to implement formal systems on a machine. Zbl 0784.68072
Avron, Arnon; Honsell, Furio; Mason, Ian A.; Pollack, Robert
1992
Deduction in non-Horn databases. Zbl 0614.68072
1985
Automatic discovery of theorems in elementary geometry. Zbl 0941.03010
Recio, T.; Vélez, M. P.
1999
Eliminating dublication with the hyper-linking strategy. Zbl 0784.68077
Lee, Shie-Jue; Plaisted, David A.
1992
Differential dynamic logic for hybrid systems. Zbl 1181.03035
Platzer, André
2008
Computing circumscription revisited: A reduction algorithm. Zbl 0939.03033
Doherty, Patrick; Łukaszewicz, Witold; Szałas, Andrzej
1997
Learning-assisted automated reasoning with $$\mathsf{Flyspeck}$$. Zbl 1314.68283
Kaliszyk, Cezary; Urban, Josef
2014
Translating higher-order clauses to first-order clauses. Zbl 1203.68188
Meng, Jia; Paulson, Lawrence C.
2008
MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095
Urban, Josef
2006
Some lambda calculus and type theory formalized. Zbl 0940.03019
McKinna, James; Pollack, Robert
1999
An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. Zbl 1002.68165
Cadoli, Marco; Schaerf, Marco; Giovanardi, Andrea; Giovanardi, Massimo
2002
Model-theoretic methods in combined constraint satisfiability. Zbl 1069.03008
Ghilardi, Silvio
2004
MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206
2010
ATP and presentation service for Mizar formalizations. Zbl 1260.68380
Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff
2013
lean$$T^ AP$$: Lean tableau-based deduction. Zbl 0838.68097
Beckert, Bernhard; Posegga, Joachim
1995
Extending Sledgehammer with SMT solvers. Zbl 1314.68272
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
2013
Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217
Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef
2014
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
2015
A logic for reasoning with inconsistency. Zbl 0807.03019
Kifer, Michael; Lozinskii, Eliezer L.
1992
Set theory for verification. I: From foundations to functions. Zbl 0802.68128
Paulson, Lawrence C.
1993
First-order modal tableaux. Zbl 0648.03004
Fitting, Melvin
1988
Non-Horn clause logic programming without contrapositives. Zbl 0666.68091
Plaisted, David A.
1988
Backdoor sets of quantified Boolean formulas. Zbl 1191.68353
Samer, Marko; Szeider, Stefan
2009
A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142
Harrison, J.; Théry, L.
1998
Branching rules for satisfiability. Zbl 0838.68098
Hooker, J. N.; Vinay, V.
1995
Locales: a module system for mathematical theories. Zbl 1315.68218
Ballarin, Clemens
2014
Explicit representation of terms defined by counter examples. Zbl 0641.68124
Lassez, J.-L.; Marriott, K.
1987
A formally verified compiler back-end. Zbl 1185.68215
Leroy, Xavier
2009
MPTP-motivation, implementation, first experiments. Zbl 1075.68081
Urban, Josef
2004
Implicit induction in conditional theories. Zbl 0819.68114
1995
New worst-case upper bounds for SAT. Zbl 0960.03009
Hirsch, Edward A.
2000
Testing positiveness of polynomials. Zbl 0916.68084
Hong, Hoon; Jakuš, Dalibor
1998
Experiments with discrimination-tree indexing and path indexing for term retrieval. Zbl 0781.68101
McCune, William
1992
Complexity of unification problems with associative-commutative operators. Zbl 0781.68076
Kapur, Deepak; Narendran, Paliath
1992
Gentzen-type systems, resolution and tableaux. Zbl 0788.03013
Avron, Arnon
1993
Stochastic Boolean satisfiability. Zbl 0988.68189
Littman, Michael L.; Majercik, Stephen M.; Pitassi, Toniann
2001
Set theory in first-order logic: Clauses for Gödel’s axioms. Zbl 0635.03008
Boyer, Robert; Lusk, Ewing; McCune, William; Overbeek, Ross; Stickel, Mark E.; Wos, Lawrence
1986
From bisimulation to simulation: Coarsest partition problems. Zbl 1081.68052
Gentilini, R.; Piazza, C.; Policriti, A.
2003
Plaisted, David A.; Zhu, Yunshan
2000
Automated theorem proving in GeoGebra: current achievements. Zbl 1356.68181
Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon
2015
Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Zbl 1109.68098
Alekhnovich, Michael; Hirsch, Edward A.; Itsykson, Dmitry
2005
On equivalents of well-foundedness. An experiment in MIZAR. Zbl 0944.68168
Rudnicki, Piotr; Trybulec, Andrzej
1999
Local search algorithms for SAT: An empirical evaluation. Zbl 0961.68039
Hoos, Holger H.; Stützle, Thomas
2000
Positive unit hyperresolution tableaux and their application to minimal model generation. Zbl 0960.03006
2000
A semantical framework for supporting subjective and conditional probabilities in deductive databases. Zbl 0784.68082
Ng, Raymond; Subrahmanian, V. S.
1993
Single axioms for groups and abelian groups with various operations. Zbl 0794.20002
McCune, William W.
1993
Autarkic computations in formal proofs. Zbl 1002.68156
Barendregt, Henk; Barendsen, Erik
2002
Priorities on defaults with prerequisites, and their application in treating specificity in terminological default logic. Zbl 0842.68081
1995
Proving geometry theorems with rewrite rules. Zbl 0642.68162
Chou, Shang-Ching; Schelter, William F.
1986
On the declarative and procedural semantics of logic programs. Zbl 0681.68109
Przymusinski, Teodor C.
1989
Weak generalized closed world assumption. Zbl 0683.68086
Rajasekar, Arcot; Lobo, Jorge; Minker, Jack
1989
Combining nonstably infinite theories. Zbl 1108.03014
Tinelli, Cesare; Zarba, Calogero G.
2005
The area method. A recapitulation. Zbl 1242.68281
Janičić, Predrag; Narboux, Julien; Quaresma, Pedro
2012
Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. Zbl 1252.68252
Felty, Amy; Momigliano, Alberto
2012
A two-level logic approach to reasoning about computations. Zbl 1290.68088
Gacek, Andrew; Miller, Dale; Nadathur, Gopalan
2012
Logical cryptanalysis as a SAT problem: Encoding and analysis of the U. S. Data Encryption Standard. Zbl 0968.68052
Massacci, Fabio; Marraro, Laura
2000
A deductive database approach to automated geometry theorem proving and discovering. Zbl 0961.68121
Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong
2000
Reachability analysis over term rewriting systems. Zbl 1075.68038
Feuillade, Guillaume; Genet, Thomas; Viet Triem Tong, Valérie
2004
Abstract congruence closure. Zbl 1040.03006
Bachmair, Leo; Tiwari, Ashish; Vigneron, Laurent
2003
Data complexity of query answering in expressive description logics via tableaux. Zbl 1154.68102
Ortiz, Magdalena; Calvanese, Diego; Eiter, Thomas
2008
Inferring negative information from disjunctive databases. Zbl 0662.68101
Ross, Kenneth A.; Topor, Rodney W.
1988
TABLEAUX: A general theorem prover for modal logics. Zbl 0743.03008
Catach, Laurent
1991
User interaction with the Matita proof assistant. Zbl 1132.68673
Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano
2007
On rewriting rules in Mizar. Zbl 1260.68376
Korniłowicz, Artur
2013
Single step tableaux for modal logics. Computational properties, complexity and methodology. Zbl 0951.03008
Massacci, Fabio
2000
Implementing the Davis-Putnam method. Zbl 0967.68148
Zhang, Hantao; Stickel, Mark
2000
A new approach for automatic theorem proving in real geometry. Zbl 0914.03013
Dolzmann, Andreas; Sturm, Thomas; Weispfenning, Volker
1998
Word unification and transformation of generalized equations. Zbl 0802.68136
Schulz, Klaus U.
1993
Proof strategies in linear logic. Zbl 0821.03004
Tammet, Tanel
1994
The liberalized $$\delta$$-rule in free variable semantic tableaux. Zbl 0826.03005
Hähnle, Reiner; Schmitt, Peter H.
1994
A comparison of Mizar and Isar. Zbl 1064.68083
Wenzel, Markus; Wiedijk, Freek
2002
Unification in abelian semigroups. Zbl 0637.68106
Herold, Alexander; Siekmann, Jörg H.
1987
A more expressive formulation of many sorted logic. Zbl 0642.68166
Cohn, Anthony G.
1987
Stable and extension class theory for logic programs and default logics. Zbl 0763.03017
Baral, Chitta R.; Subrahmanian, V. S.
1992
A graphical user interface for formal proofs in geometry. Zbl 1131.68094
Narboux, Julien
2007
OptiMathSAT: a tool for optimization modulo theories. Zbl 07176604
Sebastiani, Roberto; Trentin, Patrick
2020
Strong extension-free proof systems. Zbl 07176609
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin
2020
Probably partially true: satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. Zbl 07268902
Finger, Marcelo; Preto, Sandro
2020
Using well-founded relations for proving operational termination. Zbl 07176596
2020
Combining induction and saturation-based theorem proving. Zbl 07176598
Echenim, M.; Peltier, N.
2020
Solving quantifier-free first-order constraints over finite sets and binary relations. Zbl 07176599
Cristiá, Maximiliano; Rossi, Gianfranco
2020
A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 07176602
Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
2020
The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques. Zbl 1459.68092
Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl
2020
A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 07187044
Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
2020
Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Zbl 1441.03011
Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal
2019
Verifying OpenJDK’s sort method for generic collections. Zbl 07024053
de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic
2019
System-level non-interference of constant-time cryptography. I: Model. Zbl 1459.68026
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos
2019
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Zbl 07024052
Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.
2019
Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. Zbl 07038739
Marić, Filip
2019
Goal-oriented proof-search in natural deduction for intuitionistic propositional logic. Zbl 07024054
Ferrari, Mauro; Fiorentini, Camillo
2019
Proof pearl: Bounding least common multiples with triangles. Zbl 07024455
Chan, Hing-Lun; Norrish, Michael
2019
From types to sets by local type definition in higher-order logic. Zbl 07024458
Kunčar, Ondřej; Popescu, Andrei
2019
Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 07024459
Lammich, Peter; Sefidgar, S. Reza
2019
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Zbl 07038740
Charguéraud, Arthur; Pottier, François
2019
A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data. Zbl 1465.68041
Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre
2019
Refinement to imperative HOL. Zbl 1465.68291
Lammich, Peter
2019
A consistent foundation for Isabelle/HOL. Zbl 1465.68289
Kunčar, Ondřej; Popescu, Andrei
2019
On the generation of quantified lemmas. Zbl 1459.03011
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel
2019
Canonicity for cubical type theory. Zbl 07096713
Huber, Simon
2019
Guarded cubical type theory. Zbl 07096714
Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea
2019
The James construction and $$\pi _4(\mathbb{S}^{3})$$ in homotopy type theory. Zbl 07096715
Brunerie, Guillaume
2019
From signatures to monads in UniMath. Zbl 07096716
Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders
2019
Call-by-value lambda calculus as a model of computation in Coq. Zbl 07096721
Forster, Yannick; Smolka, Gert
2019
Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. Zbl 07100457
Beyersdorff, Olaf; Blinkhorn, Joshua; Chew, Leroy; Schmidt, Renate; Suda, Martin
2019
Classification of finite fields with applications. Zbl 07100459
Chan, Hing-Lun; Norrish, Michael
2019
Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 07100460
Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter
2019
Formalization of metatheory of the Quipper quantum programming language in a linear logic. Zbl 07121996
Mahmoud, Mohamed Yousri; Felty, Amy P.
2019
Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants. Zbl 07121998
Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.
2019
Compositional falsification of cyber-physical systems with machine learning components. Zbl 07121999
Dreossi, Tommaso; Donzé, Alexandre; Seshia, Sanjit A.
2019
Efficient active automata learning via mutation testing. Zbl 07122002
Aichernig, Bernhard K.; Tappler, Martin
2019
The role of the Mizar mathematical library for interactive proof development in Mizar. Zbl 1433.68530
Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol
2018
Automatic synthesis of logical models for order-sorted first-order theories. Zbl 1398.68095
2018
Formal verification of an executable LTL model checker with partial order reduction. Zbl 1426.68162
Brunner, Julian; Lammich, Peter
2018
Hammer for Coq: automation for dependent type theory. Zbl 1448.68458
Czajka, Łukasz; Kaliszyk, Cezary
2018
Synthesis of obfuscation policies to ensure privacy and utility. Zbl 1426.68085
Wu, Yi-Chin; Raman, Vasumathi; Rawlings, Blake C.; Lafortune, Stéphane; Seshia, Sanjit A.
2018
A formalization of metric spaces in HOL Light. Zbl 1425.68376
Maggesi, Marco
2018
Automated verification of functional correctness of race-free GPU programs. Zbl 1426.68054
Kojima, Kensuke; Imanishi, Akifumi; Igarashi, Atsushi
2018
Toward compositional verification of interruptible OS kernels and device drivers. Zbl 1451.68170
Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui
2018
Visibly linear temporal logic. Zbl 1425.68182
Bozzelli, Laura; Sánchez, César
2018
Bidirectional grammars for machine-code decoding and encoding. Zbl 1426.68069
Tan, Gang; Morrisett, Greg
2018
A unifying view on SMT-based software verification. Zbl 1426.68041
Beyer, Dirk; Dangl, Matthias; Wendler, Philipp
2018
Sentence-normalized conditional narrowing modulo in rewriting logic and Maude. Zbl 1398.68267
Aguirre, Luis; Martí-Oliet, Narciso; Palomino, Miguel; Pita, Isabel
2018
CoSMed: a confidentiality-verified social media platform. Zbl 1451.68168
Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco
2018
Verified iptables firewall analysis and verification. Zbl 1451.68173
Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg
2018
Mechanising a type-safe model of multithreaded Java with a verified compiler. Zbl 1451.68178
Lochbihler, Andreas
2018
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457
Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph
2018
Formalization of the resolution calculus for first-order logic. Zbl 1451.03019
Schlichtkrull, Anders
2018
A verified ODE solver and the Lorenz attractor. Zbl 1448.68460
Immler, Fabian
2018
A synthetic proof of Pappus’ theorem in Tarski’s geometry. Zbl 1405.03034
Braun, Gabriel; Narboux, Julien
2017
Analyzing program termination and complexity automatically with AProVE. Zbl 1409.68255
Giesl, 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é
2017
A fully automatic theorem prover with human-style output. Zbl 1405.03035
Ganesalingam, M.; Gowers, W. T.
2017
A formally verified proof of the central limit theorem. Zbl 1425.68369
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke
2017
Combining SAT solvers with computer algebra systems to verify combinatorial conjectures. Zbl 1410.68413
Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay
2017
Soundness and completeness proofs by coinductive methods. Zbl 1409.68251
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
2017
Finding proofs in Tarskian geometry. Zbl 1414.68100
Beeson, Michael; Wos, Larry
2017
The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. Zbl 1425.68381
Sutcliffe, Geoff
2017
A semantic framework for proof evidence. Zbl 1425.68371
Chihani, Zakaria; Miller, Dale; Renaud, Fabien
2017
Automated reducible geometric theorem proving and discovery by Gröbner basis method. Zbl 1425.68383
Zhou, Jie; Wang, Dingkang; Sun, Yao
2017
Markov chains and Markov decision processes in Isabelle/HOL. Zbl 1425.68375
Hölzl, Johannes
2017
Complexity and resource bound analysis of imperative programs using difference constraints. Zbl 1409.68076
Sinn, Moritz; Zuleger, Florian; Veith, Helmut
2017
The OWL reasoner evaluation (ORE) 2015 competition report. Zbl 1425.68402
Parsia, Bijan; Matentzoglu, Nicolas; Gonçalves, Rafael S.; Glimm, Birte; Steigmiller, Andreas
2017
Semantically-guided goal-sensitive reasoning: inference system and completeness. Zbl 1437.68189
Bonacina, Maria Paola; Plaisted, David A.
2017
A complete uniform substitution calculus for differential dynamic logic. Zbl 1437.03119
Platzer, André
2017
On preprocessing techniques and their impact on propositional model counting. Zbl 1409.68259
Lagniez, Jean-Marie; Marquis, Pierre
2017
Proving divide and conquer complexities in Isabelle/HOL. Zbl 1414.68101
Eberl, Manuel
2017
Higher-order pattern anti-unification in linear time. Zbl 1407.68089
Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu
2017
Automatically proving termination and memory safety for programs with pointer arithmetic. Zbl 1409.68077
Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius
2017
Formally proving size optimality of sorting networks. Zbl 1425.68372
Cruz-Filipe, Luís; Larsen, Kim S.; Schneider-Kamp, Peter
2017
Preface: Special issue on automatic resource bound analysis. Zbl 1368.00054
Giesl, Jürgen; Hoffmann, Jan
2017
Type-based cost analysis for lazy functional languages. Zbl 1409.68067
Jost, Steffen; Vasconcelos, Pedro; Florido, Mário; Hammond, Kevin
2017
Lower bounds for runtime complexity of term rewriting. Zbl 1409.68254
Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas
2017
Abstract interpretation as automated deduction. Zbl 1410.68222
D&rsquo;Silva, Vijay; Urban, Caterina
2017
The Bayesian ontology language $$\mathcal {BEL}$$. Zbl 1409.68278
Ceylan, İsmail İlkan; Peñaloza, Rafael
2017
Solution validation and extraction for QBF preprocessing. Zbl 1409.68258
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin
2017
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
2016
Semi-intelligible Isar proofs from machine-generated proofs. Zbl 1356.68178
Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert
2016
Adding decision procedures to SMT solvers using axioms with triggers. Zbl 1356.68187
Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei
2016
Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation. Zbl 1356.68194
Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott
2016
Proving tight bounds on univariate expressions with elementary functions in Coq. Zbl 1386.68151
Martin-Dorel, Érik; Melquiond, Guillaume
2016
Psi-calculi in Isabelle. Zbl 1356.68175
Bengtson, Jesper; Parrow, Joachim; Weber, Tjark
2016
Semantically-guided goal-sensitive reasoning: model representation. Zbl 1356.68180
Bonacina, Maria Paola; Plaisted, David A.
2016
On definitions of constants and types in HOL. Zbl 1356.68173
Arthan, Rob
2016
Quasi-decidability of a fragment of the first-order theory of real numbers. Zbl 1437.03047
Franek, Peter; Ratschan, Stefan; Zgliczynski, Piotr
2016
Complete instantiation-based interpolation. Zbl 1356.68203
Totla, Nishant; Wies, Thomas
2016
Eisbach: a proof method language for Isabelle. Zbl 1356.68195
Matichuk, Daniel; Murray, Toby; Wenzel, Makarius
2016
Quantifier reordering for QBF. Zbl 1356.68200
Slivovsky, Friedrich; Szeider, Stefan
2016
Formal proofs of rounding error bounds. With application to an automatic positive definiteness check. Zbl 1409.68263
Roux, Pierre
2016
Reasoning about algebraic data types with abstractions. Zbl 1386.68104
Pham, Tuan-Hung; Gacek, Andrew; Whalen, Michael W.
2016
Automated proofs of block cipher modes of operation. Zbl 1356.68188
Gagné, Martin; Lafourcade, Pascal; Lakhnech, Yassine; Safavi-Naini, Reihaneh
2016
Mechanizing a process algebra for network protocols. Zbl 1356.68182
Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter
2016
A heuristic prover for real inequalities. Zbl 1356.68174
Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody
2016
Four decades of {Mizar}. Foreword. Zbl 1336.00111
2015
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
2015
Automated theorem proving in GeoGebra: current achievements. Zbl 1356.68181
Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon
2015
The higher-order prover Leo-II. Zbl 1356.68176
Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank
2015
...and 629 more Documents
all top 5

#### Cited by 3,586 Authors

 31 Paulson, Lawrence Charles 29 Urban, Josef 27 Eiter, Thomas 25 Meseguer Guaita, José 24 Kaliszyk, Cezary 21 Benzmüller, Christoph Ewald 20 Lucas, Salvador 20 Weidenbach, Christoph 18 Blanchette, Jasmin Christian 18 Gao, Xiaoshan 18 Grabowski, Adam 18 Marques-Silva, João P. 17 Giesl, Jürgen 17 Peltier, Nicolas 17 Voronkov, Andrei 16 Korniłowicz, Artur 16 Middeldorp, Aart 14 Baader, Franz 14 Bonacina, Maria Paola 14 Gottlob, Georg 14 Subramani, Krishnan 14 Tinelli, Cesare 14 Wos, Larry 13 Ayala-Rincón, Mauricio 13 Biere, Armin 13 Bundy, Alan 13 Cantone, Domenico 13 Ghilardi, Silvio 13 Naumowicz, Adam 13 Nipkow, Tobias 13 Schaub, Torsten H. 13 Subrahmanian, V. S. 13 Sutcliffe, Geoff 13 Thiemann, René 12 Calvanese, Diego 12 Kohlhase, Michael 12 Pąk, Karol 12 Plaisted, David Alan 12 Rusinowitch, Michaël 12 Schneider-Kamp, Peter 12 Szeider, Stefan 12 Waldmann, Uwe 11 Baumgartner, Peter 11 Bonatti, Piero Andrea 11 Giunchiglia, Enrico 11 Janičić, Predrag 11 Kapur, Deepak 11 Koch, Sebastian 11 Narboux, Julien 11 Rabe, Florian 11 Smolka, Gert 11 Tahar, Sofiène 11 Wang, Dongming 10 Alviano, Mario 10 Avron, Arnon 10 Botana, Francisco 10 Kirchner, Claude 10 Kovács, Zoltán 10 Leone, Nicola 10 Maratea, Marco 10 Miller, Dale Allen 10 Montanari, Angelo 10 Platzer, André 10 Zhang, Hantao 9 Amgoud, Leila 9 Armando, Alessandro 9 Chou, Shangching 9 Echenim, Mnacho 9 Egly, Uwe 9 Felty, Amy P. 9 Gabbay, Dov M. 9 Gabbay, Murdoch James 9 Hasan, Osman 9 Horrocks, Ian 9 Kerber, Manfred 9 Kinyon, Michael K. 9 Kutsia, Temur 9 Lutz, Carsten 9 McCune, William W. 9 Nakasho, Kazuhisa 9 Narendran, Paliath 9 Nigam, Vivek 9 Omodeo, Eugenio Giovanni 9 Peñaloza, Rafael 9 Pientka, Brigitte 9 Ranise, Silvio 9 Recio, Tomas 9 Ringeissen, Christophe 9 Schmidt-Schauß, Manfred 9 Shidama, Yasunari 9 Szałas, Andrzej 9 Veroff, Robert 9 Wolter, Frank 9 Zakharyaschev, Michael Viktorovich 8 Albert, Elvira 8 Böhme, Sascha 8 Dixon, Clare 8 Dowek, Gilles 8 Farmer, William M. 8 Fernández, Maribel ...and 3,486 more Authors
all top 5

#### Cited in 201 Journals

 445 Journal of Automated Reasoning 184 Artificial Intelligence 180 Theoretical Computer Science 123 Journal of Symbolic Computation 119 Annals of Mathematics and Artificial Intelligence 77 Information and Computation 77 Formalized Mathematics 59 Theory and Practice of Logic Programming 45 Formal Aspects of Computing 44 MSCS. Mathematical Structures in Computer Science 43 Journal of Applied Logic 39 International Journal of Approximate Reasoning 37 Journal of Applied Non-Classical Logics 32 Annals of Pure and Applied Logic 30 Discrete Applied Mathematics 29 Journal of Logical and Algebraic Methods in Programming 26 Formal Methods in System Design 26 Logical Methods in Computer Science 25 Information Processing Letters 25 Mathematics in Computer Science 23 Journal of Functional Programming 23 Constraints 21 Information Sciences 21 Journal of Computer and System Sciences 20 Fuzzy Sets and Systems 19 Studia Logica 18 ACM Transactions on Computational Logic 17 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 11 The Journal of Logic and Algebraic Programming 11 Logica Universalis 10 The Journal of Symbolic Logic 10 Journal of Computer Science and Technology 8 Science of Computer Programming 8 International Journal of Computer Mathematics 7 Journal of Philosophical Logic 7 Notre Dame Journal of Formal Logic 7 AI Communications 7 JETAI. Journal of Experimental & Theoretical Artificial Intelligence 7 Computational Geometry 7 Journal of Logic, Language and Information 7 The Bulletin of Symbolic Logic 6 International Journal of General Systems 6 Mathematics and Computers in Simulation 6 Synthese 6 Computers & Operations Research 6 European Journal of Operational Research 6 Fundamenta Informaticae 6 Computer Languages, Systems & Structures 6 Prikladnaya Diskretnaya Matematika 5 International Journal of Intelligent Systems 5 Annals of Operations Research 5 Soft Computing 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 4 Communications in Algebra 4 Algorithmica 4 Mathematical and Computer Modelling 4 Indagationes Mathematicae. New Series 4 Computational Complexity 4 Journal of Mathematical Sciences (New York) 4 Theory of Computing Systems 4 LMS Journal of Computation and Mathematics 4 International Journal of Applied Mathematics and Computer Science 4 Journal of Applied Mathematics 4 The Review of Symbolic Logic 4 Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas. RACSAM 3 Automatica 3 Journal of Algebra 3 Semigroup Forum 3 Machine Learning 3 International Journal of Foundations of Computer Science 3 Archive for Mathematical Logic 3 Cybernetics and Systems Analysis 3 Journal of Heuristics 3 Mathematical Problems in Engineering 3 RAIRO. Theoretical Informatics and Applications 3 Journal of Discrete Algorithms 3 Nonlinear Analysis. Hybrid Systems 2 Discrete Mathematics 2 Mathematics of Computation 2 The Mathematical Intelligencer 2 Journal of Mathematical Economics 2 Programming and Computer Software 2 Results in Mathematics 2 Transactions of the American Mathematical Society 2 History and Philosophy of Logic 2 Order 2 Journal of Cryptology 2 Science in China. Series A 2 Pattern Recognition 2 Mathematical Logic Quarterly (MLQ) 2 The Journal of Artificial Intelligence Research (JAIR) 2 Journal of Combinatorial Optimization 2 International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems ...and 101 more Journals
all top 5

#### Cited in 51 Fields

 2,643 Computer science (68-XX) 1,086 Mathematical logic and foundations (03-XX) 98 Operations research, mathematical programming (90-XX) 78 Information and communication theory, circuits (94-XX) 59 Geometry (51-XX) 57 Numerical analysis (65-XX) 51 Combinatorics (05-XX) 42 Commutative algebra (13-XX) 40 Number theory (11-XX) 39 Order, lattices, ordered algebraic structures (06-XX) 38 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 34 Group theory and generalizations (20-XX) 27 Field theory and polynomials (12-XX) 22 General and overarching topics; collections (00-XX) 22 Algebraic geometry (14-XX) 22 Category theory; homological algebra (18-XX) 22 Systems theory; control (93-XX) 20 History and biography (01-XX) 20 Real functions (26-XX) 18 General algebraic systems (08-XX) 13 Ordinary differential equations (34-XX) 13 Algebraic topology (55-XX) 11 Statistics (62-XX) 11 Biology and other natural sciences (92-XX) 10 Linear and multilinear algebra; matrix theory (15-XX) 10 Probability theory and stochastic processes (60-XX) 10 Mathematics education (97-XX) 9 Associative rings and algebras (16-XX) 8 Dynamical systems and ergodic theory (37-XX) 8 Operator theory (47-XX) 7 Measure and integration (28-XX) 7 Partial differential equations (35-XX) 6 Special functions (33-XX) 6 Convex and discrete geometry (52-XX) 6 Mechanics of particles and systems (70-XX) 5 Quantum theory (81-XX) 3 Nonassociative rings and algebras (17-XX) 3 Approximations and expansions (41-XX) 3 Harmonic analysis on Euclidean spaces (42-XX) 3 Differential geometry (53-XX) 3 Optics, electromagnetic theory (78-XX) 2 Difference and functional equations (39-XX) 2 Integral equations (45-XX) 2 Calculus of variations and optimal control; optimization (49-XX) 2 General topology (54-XX) 2 Fluid mechanics (76-XX) 1 Functions of a complex variable (30-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Sequences, series, summability (40-XX) 1 Functional analysis (46-XX) 1 Mechanics of deformable solids (74-XX)