×

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,083 Publications (since 1985)
References Indexed: 747 Publications with 25,430 References.
all top 5

Latest Issues

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

Authors

38 Wos, Larry
19 Paulson, Lawrence Charles
14 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 Bonacina, Maria Paola
8 Kaliszyk, Cezary
8 Kaufmann, Matt
8 Moore, J Strother
8 Norrish, Michael
8 Veroff, Robert
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 Popescu, Andrei
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 Lucas, Salvador
5 Miller, Dale Allen
5 Narendran, Paliath
5 Ohlbach, Hans Jürgen
5 Schmidt, Renate A.
5 Smolka, Gert
5 Subrahmanian, V. S.
5 Weidenbach, Christoph
5 Zhang, Jingzhong
4 Andrews, Peter B.
4 Ayala-Rincón, Mauricio
4 Barrett, Clark W.
4 Barthe, Gilles
4 Bledsoe, Woodrow W.
4 Böhme, Sascha
4 Cialdea Mayer, Marta
4 Cristiá, Maximiliano
4 Delaune, Stéphanie
4 Fiorino, Guido
4 Fitelson, Branden
4 Gamboa, Ruben A.
4 Ghilardi, Silvio
4 Giunchiglia, Fausto
4 Heule, Marijn J. H.
4 Janičić, Predrag
4 Klein, Gerwin
4 Kohlhase, Michael
4 Korniłowicz, Artur
4 Kremer, Steve
4 Lochbihler, Andreas
4 Loveland, Donald W.
4 Lu, James J.
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 Rossi, Gianfranco
4 Rudnicki, Piotr
4 Ruiz-Reina, José-Luis
4 Schulz, Stephan
4 Sebastiani, Roberto
4 Suttner, Christian B.
4 Szeider, Stefan
4 Théry, Laurent
...and 1,388 more Authors
all top 5

Fields

1,001 Computer science (68-XX)
439 Mathematical logic and foundations (03-XX)
37 General and overarching topics; collections (00-XX)
29 Information and communication theory, circuits (94-XX)
19 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)
7 Commutative algebra (13-XX)
7 Category theory; homological algebra (18-XX)
5 Algebraic topology (55-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 Quantum theory (81-XX)
3 Systems theory; control (93-XX)
2 Linear and multilinear algebra; matrix theory (15-XX)
2 Associative rings and algebras (16-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)
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)

Publications by Year

Citations contained in zbMATH Open

789 Publications have been cited 5,823 times in 3,545 Documents Cited by Year
The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0. Zbl 1185.68636
Sutcliffe, Geoff
95
2009
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
92
2007
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
79
2018
Four decades of {Mizar}. Foreword. Zbl 1336.00111
63
2015
The TPTP problem library. CNF release v1. 2. 1. Zbl 0910.68197
Sutcliffe, Geoff; Suttner, Christian
59
1998
Basic principles of mechanical theorem proving in elementary geometries. Zbl 0642.68163
Wu, Wentsun
58
1986
Theorem proving modulo. Zbl 1049.03011
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
52
2003
Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Zbl 0967.68145
Gomes, Carla P.; Selman, Bart; Crato, Nuno; Kautz, Henry
48
2000
Nominal techniques in Isabelle/HOL. Zbl 1140.68061
Urban, Christian
48
2008
The foundation of a generic theorem prover. Zbl 0679.68173
Paulson, Lawrence C.
47
1989
Mechanizing and improving dependency pairs. Zbl 1113.68088
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan
47
2006
Algorithms for computing minimal unsatisfiable subsets of constraints. Zbl 1154.68510
Liffiton, Mark H.; Sakallah, Karem A.
46
2008
SETHEO: A high-performance theorem prover. Zbl 0759.68080
Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W.
45
1992
Solution of the Robbins problem. Zbl 0883.06011
McCune, William
45
1997
A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Zbl 0662.68104
Stickel, Mark E.
44
1988
Automated deduction by theory resolution. Zbl 0616.68076
Stickel, Mark E.
43
1985
Matrix interpretations for proving termination of term rewriting. Zbl 1139.68049
Endrullis, Jörg; Waldmann, Johannes; Zantema, Hans
43
2008
Seventy-five problems for testing automatic theorem provers. Zbl 0642.68147
Pelletier, Francis Jeffry
36
1986
Answer set programming based on propositional satisfiability. Zbl 1107.68029
Giunchiglia, Enrico; Lierler, Yuliya; Maratea, Marco
36
2006
Differential dynamic logic for hybrid systems. Zbl 1181.03035
Platzer, André
35
2008
A tableau decision procedure for \(\mathcal{SHOIQ}\). Zbl 1132.68734
Horrocks, Ian; Sattler, Ulrike
34
2007
MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095
Urban, Josef
34
2006
Inferring from inconsistency in preference-based argumentation frameworks. Zbl 1056.68589
Amgoud, Leila; Cayrol, Claudette
34
2002
Controlled integration of the cut rule into connection tableau calculi. Zbl 0816.03005
Letz, R.; Mayr, K.; Goller, C.
33
1994
Translating higher-order clauses to first-order clauses. Zbl 1203.68188
Meng, Jia; Paulson, Lawrence C.
32
2008
Productive use of failure in inductive proof. Zbl 0847.68103
Ireland, Andrew; Bundy, Alan
31
1996
The HOL Light theory of Euclidean space. Zbl 1260.68373
Harrison, John
30
2013
IMPS: An interactive mathematical proof system. Zbl 0802.68129
Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier
30
1993
Using typed lambda calculus to implement formal systems on a machine. Zbl 0784.68072
Avron, Arnon; Honsell, Furio; Mason, Ian A.; Pollack, Robert
29
1992
Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217
Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef
29
2014
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
28
2015
ATP and presentation service for Mizar formalizations. Zbl 1260.68380
Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff
28
2013
Automatic discovery of theorems in elementary geometry. Zbl 0941.03010
Recio, T.; Vélez, M. P.
28
1999
Model-theoretic methods in combined constraint satisfiability. Zbl 1069.03008
Ghilardi, Silvio
28
2004
Extending Sledgehammer with SMT solvers. Zbl 1314.68272
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
28
2013
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283
Kaliszyk, Cezary; Urban, Josef
28
2014
The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. Zbl 1425.68381
Sutcliffe, Geoff
27
2017
Deduction in non-Horn databases. Zbl 0614.68072
Yahya, Adnan; Henschen, Lawrence J.
27
1985
Eliminating dublication with the hyper-linking strategy. Zbl 0784.68077
Lee, Shie-Jue; Plaisted, David A.
25
1992
MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206
Akbarpour, Behzad; Paulson, Lawrence Charles
25
2010
An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. Zbl 1002.68165
Cadoli, Marco; Schaerf, Marco; Giovanardi, Andrea; Giovanardi, Massimo
24
2002
Computing circumscription revisited: A reduction algorithm. Zbl 0939.03033
Doherty, Patrick; Łukaszewicz, Witold; Szałas, Andrzej
24
1997
lean\(T^ AP\): Lean tableau-based deduction. Zbl 0838.68097
Beckert, Bernhard; Posegga, Joachim
24
1995
Backdoor sets of quantified Boolean formulas. Zbl 1191.68353
Samer, Marko; Szeider, Stefan
23
2009
A formally verified compiler back-end. Zbl 1185.68215
Leroy, Xavier
23
2009
Some lambda calculus and type theory formalized. Zbl 0940.03019
McKinna, James; Pollack, Robert
23
1999
Experiments with discrimination-tree indexing and path indexing for term retrieval. Zbl 0781.68101
McCune, William
23
1992
Locales: a module system for mathematical theories. Zbl 1315.68218
Ballarin, Clemens
23
2014
A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142
Harrison, J.; Théry, L.
22
1998
Set theory for verification. I: From foundations to functions. Zbl 0802.68128
Paulson, Lawrence C.
22
1993
Logical cryptanalysis as a SAT problem: Encoding and analysis of the U. S. Data Encryption Standard. Zbl 0968.68052
Massacci, Fabio; Marraro, Laura
21
2000
Non-Horn clause logic programming without contrapositives. Zbl 0666.68091
Plaisted, David A.
21
1988
A logic for reasoning with inconsistency. Zbl 0807.03019
Kifer, Michael; Lozinskii, Eliezer L.
21
1992
Explicit representation of terms defined by counter examples. Zbl 0641.68124
Lassez, J.-L.; Marriott, K.
21
1987
First-order modal tableaux. Zbl 0648.03004
Fitting, Melvin
21
1988
Branching rules for satisfiability. Zbl 0838.68098
Hooker, J. N.; Vinay, V.
21
1995
New worst-case upper bounds for SAT. Zbl 0960.03009
Hirsch, Edward A.
20
2000
Stochastic Boolean satisfiability. Zbl 0988.68189
Littman, Michael L.; Majercik, Stephen M.; Pitassi, Toniann
20
2001
Complexity of unification problems with associative-commutative operators. Zbl 0781.68076
Kapur, Deepak; Narendran, Paliath
20
1992
MPTP-motivation, implementation, first experiments. Zbl 1075.68081
Urban, Josef
20
2004
On the declarative and procedural semantics of logic programs. Zbl 0681.68109
Przymusinski, Teodor C.
19
1989
Testing positiveness of polynomials. Zbl 0916.68084
Hong, Hoon; Jakuš, Dalibor
19
1998
Gentzen-type systems, resolution and tableaux. Zbl 0788.03013
Avron, Arnon
19
1993
Implicit induction in conditional theories. Zbl 0819.68114
Bouhoula, Adel; Rusinowitch, Michaël
19
1995
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
18
2015
Closed-form upper bounds in static cost analysis. Zbl 1213.68200
Albert, Elvira; Arenas, Puri; Genaim, Samir; Puebla, Germán
18
2011
A two-level logic approach to reasoning about computations. Zbl 1290.68088
Gacek, Andrew; Miller, Dale; Nadathur, Gopalan
18
2012
Local search algorithms for SAT: An empirical evaluation. Zbl 0961.68039
Hoos, Holger H.; Stützle, Thomas
18
2000
A deductive database approach to automated geometry theorem proving and discovering. Zbl 0961.68121
Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong
18
2000
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
18
1986
Combining nonstably infinite theories. Zbl 1108.03014
Tinelli, Cesare; Zarba, Calogero G.
18
2005
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é
18
2017
Stable and extension class theory for logic programs and default logics. Zbl 0763.03017
Baral, Chitta R.; Subrahmanian, V. S.
17
1992
Positive unit hyperresolution tableaux and their application to minimal model generation. Zbl 0960.03006
Bry, François; Yahya, Adnan
17
2000
Ordered semantic hyper-linking. Zbl 0959.68115
Plaisted, David A.; Zhu, Yunshan
17
2000
Autarkic computations in formal proofs. Zbl 1002.68156
Barendregt, Henk; Barendsen, Erik
17
2002
Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. Zbl 1252.68252
Felty, Amy; Momigliano, Alberto
17
2012
Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Zbl 1109.68098
Alekhnovich, Michael; Hirsch, Edward A.; Itsykson, Dmitry
17
2005
A logical characterization of forward and backward chaining in the inverse method. Zbl 1151.03006
Chaudhuri, Kaustuv; Pfenning, Frank; Price, Greg
17
2008
The ILTP problem library for intuitionistic logic. Zbl 1113.68093
Raths, Thomas; Otten, Jens; Kreitz, Christoph
17
2007
Priorities on defaults with prerequisites, and their application in treating specificity in terminological default logic. Zbl 0842.68081
Baader, Franz; Hollunder, Bernhard
17
1995
From bisimulation to simulation: Coarsest partition problems. Zbl 1081.68052
Gentilini, R.; Piazza, C.; Policriti, A.
17
2003
On rewriting rules in Mizar. Zbl 1260.68376
Korniłowicz, Artur
16
2013
The locally nameless representation. Zbl 1260.68368
Charguéraud, Arthur
16
2012
On equivalents of well-foundedness. An experiment in MIZAR. Zbl 0944.68168
Rudnicki, Piotr; Trybulec, Andrzej
16
1999
Weak generalized closed world assumption. Zbl 0683.68086
Rajasekar, Arcot; Lobo, Jorge; Minker, Jack
16
1989
Using hints to increase the effectiveness of an automated reasoning program: Case studies. Zbl 0857.68095
Veroff, Robert
16
1996
TPS: A theorem-proving system for classical type theory. Zbl 0858.03017
Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei
16
1996
Dualities between alternative semantics for logic programming and nonmonotonic reasoning. Zbl 0782.68074
Baral, Chitta R.; Subrahmanian, V. S.
16
1993
A semantical framework for supporting subjective and conditional probabilities in deductive databases. Zbl 0784.68082
Ng, Raymond; Subrahmanian, V. S.
16
1993
Single axioms for groups and abelian groups with various operations. Zbl 0794.20002
McCune, William W.
16
1993
The area method. A recapitulation. Zbl 1242.68281
Janičić, Predrag; Narboux, Julien; Quaresma, Pedro
16
2012
Proving geometry theorems with rewrite rules. Zbl 0642.68162
Chou, Shang-Ching; Schelter, William F.
16
1986
Inferring negative information from disjunctive databases. Zbl 0662.68101
Ross, Kenneth A.; Topor, Rodney W.
16
1988
The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies. Zbl 1331.68216
Kazakov, Yevgeny; Krötzsch, Markus; Simančík, František
16
2014
Mechanically proving termination using polynomial interpretations. Zbl 1108.03017
Contejean, Evelyne; Marché, Claude; Tomás, Ana Paula; Urbain, Xavier
16
2005
TABLEAUX: A general theorem prover for modal logics. Zbl 0743.03008
Catach, Laurent
15
1991
Mechanizing complemented lattices within Mizar type system. Zbl 1356.68189
Grabowski, Adam
15
2015
The higher-order prover Leo-II. Zbl 1356.68176
Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank
15
2015
Mechanized semantics for the clight subset of the C language. Zbl 1185.68136
Blazy, Sandrine; Leroy, Xavier
15
2009
Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL. Zbl 07498609
Huerta y Munive, Jonathan Julián; Struth, Georg
1
2022
TacticToe: learning to prove with tactics. Zbl 07356973
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael
5
2021
Automated proof of Bell-LaPadula security properties. Zbl 07356979
Cristiá, Maximiliano; Rossi, Gianfranco
4
2021
Machine learning guidance for connection tableaux. Zbl 07356974
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
3
2021
Building strategies into QBF proofs. Zbl 07356969
Beyersdorff, Olaf; Blinkhorn, Joshua; Mahajan, Meena
2
2021
Automated reasoning with restricted intensional sets. Zbl 07432188
Cristiá, Maximiliano; Rossi, Gianfranco
2
2021
Superposition with lambdas. Zbl 07433023
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe
2
2021
Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 07356971
Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel
1
2021
On the importance of domain model configuration for automated planning engines. Zbl 07432186
Vallati, Mauro; Chrpa, Lukáš; McCluskey, Thomas Leo; Hutter, Frank
1
2021
Optimization modulo the theories of signed bit-vectors and floating-point numbers. Zbl 07433028
Trentin, Patrick; Sebastiani, Roberto
1
2021
An automatically verified prototype of the Tokeneer ID station specification. Zbl 07461267
Cristiá, Maximiliano; Rossi, Gianfranco
1
2021
Experiences from exporting major proof assistant libraries. Zbl 07461271
Kohlhase, Michael; Rabe, Florian
1
2021
Solving quantifier-free first-order constraints over finite sets and binary relations. Zbl 1468.03009
Cristiá, Maximiliano; Rossi, Gianfranco
5
2020
OptiMathSAT: a tool for optimization modulo theories. Zbl 1468.68206
Sebastiani, Roberto; Trentin, Patrick
5
2020
Scalable fine-grained proofs for formula processing. Zbl 1468.68278
Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal
4
2020
Strong extension-free proof systems. Zbl 1468.03011
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin
4
2020
The MetaCoq project. Zbl 1468.68075
Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo
4
2020
A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 1469.68165
Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
3
2020
Efficient verified (UN)SAT certificate checking. Zbl 1468.68134
Lammich, Peter
3
2020
Exploring the structure of an algebra text with locales. Zbl 1468.68277
Ballarin, Clemens
3
2020
Probably partially true: satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. Zbl 1468.68200
Finger, Marcelo; Preto, Sandro
3
2020
Using well-founded relations for proving operational termination. Zbl 1468.03034
Lucas, Salvador
2
2020
Blocking and other enhancements for bottom-up model generation methods. Zbl 1468.68279
Baumgartner, Peter; Schmidt, Renate A.
2
2020
\(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments. Zbl 1468.68304
Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare
2
2020
Conflict-driven satisfiability for theory combination: transition system and completeness. Zbl 1468.68194
Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan
2
2020
Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307
Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe
2
2020
System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David
2
2020
A formalized general theory of syntax with bindings: extended version. Zbl 1468.68073
Gheri, Lorenzo; Popescu, Andrei
1
2020
Automating free logic in HOL, with an experimental application in category theory. Zbl 1434.68639
Benzmüller, Christoph; Scott, Dana S.
1
2020
Politeness and combination methods for theories with bridging functions. Zbl 1468.68143
Chocron, Paula; Fontaine, Pascal; Ringeissen, Christophe
1
2020
Combining induction and saturation-based theorem proving. Zbl 1476.68300
Echenim, M.; Peltier, N.
1
2020
A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 1468.68326
Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
2020
Automatically verifying temporal properties of pointer programs with cyclic proof. Zbl 1468.68137
Tellez, Gadi; Brotherston, James
1
2020
First-order automated reasoning with theories: when deduction modulo theory meets practice. Zbl 1468.68282
Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier
1
2020
Constructive decision via redundancy-free proof-search. Zbl 1468.03015
Larchey-Wendling, Dominique
1
2020
Parameterized model checking on the TSO weak memory model. Zbl 1468.68123
Conchon, Sylvain; Declerck, David; Zaïdi, Fatiha
1
2020
Multi-cost bounded tradeoff analysis in MDP. Zbl 1468.68132
Hartmanns, Arnd; Junges, Sebastian; Katoen, Joost-Pieter; Quatmann, Tim
1
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
1
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
6
2019
Canonicity for cubical type theory. Zbl 1477.03036
Huber, Simon
6
2019
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Zbl 1468.68120
Charguéraud, Arthur; Pottier, François
5
2019
A consistent foundation for Isabelle/HOL. Zbl 1465.68289
Kunčar, Ondřej; Popescu, Andrei
5
2019
The univalence axiom in cubical sets. Zbl 07096712
Bezem, Marc; Coquand, Thierry; Huber, Simon
5
2019
Verifying OpenJDK’s sort method for generic collections. Zbl 1468.68125
de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic
4
2019
Refinement to imperative HOL. Zbl 1465.68291
Lammich, Peter
4
2019
Guarded cubical type theory. Zbl 1477.03034
Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea
4
2019
System-level non-interference of constant-time cryptography. I: Model. Zbl 1459.68026
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos
3
2019
From types to sets by local type definition in higher-order logic. Zbl 1468.68295
Kunčar, Ondřej; Popescu, Andrei
3
2019
Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 1468.68328
Lammich, Peter; Sefidgar, S. Reza
3
2019
Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. Zbl 1468.03008
Beyersdorff, Olaf; Blinkhorn, Joshua; Chew, Leroy; Schmidt, Renate; Suda, Martin
3
2019
On the generation of quantified lemmas. Zbl 1459.03011
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel
2
2019
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Zbl 1468.68298
Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.
2
2019
The flow of ODEs: formalization of variational equation and Poincaré map. Zbl 1468.68325
Immler, Fabian; Traut, Christoph
2
2019
Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. Zbl 1468.68302
Marić, Filip
2
2019
Amortized complexity verified. Zbl 1465.68060
Nipkow, Tobias; Brinkop, Hauke
2
2019
The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory. Zbl 1477.03035
Brunerie, Guillaume
2
2019
Semantics of Mizar as an Isabelle object logic. Zbl 1468.68290
Kaliszyk, Cezary; Pąk, Karol
2
2019
Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 1468.68318
Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter
2
2019
Formalization of geometric algebra in HOL Light. Zbl 1468.68329
Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong
2
2019
A proof theory for model checking. Zbl 1468.03078
Heath, Quentin; Miller, Dale
2
2019
QPCF: higher-order languages and quantum circuits. Zbl 1468.68049
Paolini, Luca; Piccolo, Mauro; Zorzi, Margherita
2
2019
Formalization of metatheory of the Quipper quantum programming language in a linear logic. Zbl 1468.68330
Mahmoud, Mohamed Yousri; Felty, Amy P.
2
2019
Compositional falsification of cyber-physical systems with machine learning components. Zbl 1468.68126
Dreossi, Tommaso; Donzé, Alexandre; Seshia, Sanjit A.
2
2019
Automatic refinement to efficient data structures: a comparison of two approaches. Zbl 1459.68228
Lammich, Peter; Lochbihler, Andreas
1
2019
Goal-oriented proof-search in natural deduction for intuitionistic propositional logic. Zbl 1474.03067
Ferrari, Mauro; Fiorentini, Camillo
1
2019
Proof pearl: Bounding least common multiples with triangles. Zbl 1468.68284
Chan, Hing-Lun; Norrish, Michael
1
2019
Formally verified approximations of definite integrals. Zbl 1468.68301
Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas
1
2019
Extraction of expansion trees. Zbl 1468.68296
Leitsch, Alexander; Lolic, Anela
1
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
1
2019
From signatures to monads in UniMath. Zbl 1468.03007
Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders
1
2019
A formalization of convex polyhedra based on the simplex method. Zbl 1468.68316
Allamigeon, Xavier; Katz, Ricardo D.
1
2019
Call-by-value lambda calculus as a model of computation in Coq. Zbl 1468.68323
Forster, Yannick; Smolka, Gert
1
2019
Categoricity results and large model constructions for second-order ZF in dependent type theory. Zbl 1468.03013
Kirst, Dominik; Smolka, Gert
1
2019
Effect polymorphism in higher-order logic (proof pearl). Zbl 1468.68062
Lochbihler, Andreas
1
2019
Classification of finite fields with applications. Zbl 1468.68317
Chan, Hing-Lun; Norrish, Michael
1
2019
An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68313
Abdulaziz, Mohammad; Paulson, Lawrence C.
1
2019
Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants. Zbl 1468.68135
Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.
1
2019
Explaining AI decisions using efficient methods for learning sparse Boolean formulae. Zbl 1468.68149
Jha, Susmit; Sahai, Tuhin; Raman, Vasumathi; Pinto, Alessandro; Francis, Michael
1
2019
An automata-theoretic approach to model-checking systems and specifications over infinite data domains. Zbl 1468.68128
Frenkel, Hadar; Grumberg, Orna; Sheinvald, Sarai
1
2019
Efficient active automata learning via mutation testing. Zbl 1468.68117
Aichernig, Bernhard K.; Tappler, Martin
1
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
79
2018
Hammer for Coq: automation for dependent type theory. Zbl 1448.68458
Czajka, Łukasz; Kaliszyk, Cezary
10
2018
Automatic synthesis of logical models for order-sorted first-order theories. Zbl 1398.68095
Lucas, Salvador; Gutiérrez, Raúl
7
2018
Formal verification of an executable LTL model checker with partial order reduction. Zbl 1426.68162
Brunner, Julian; Lammich, Peter
5
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.
5
2018
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457
Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph
4
2018
A verified ODE solver and the Lorenz attractor. Zbl 1448.68460
Immler, Fabian
3
2018
Automated verification of functional correctness of race-free GPU programs. Zbl 1426.68054
Kojima, Kensuke; Imanishi, Akifumi; Igarashi, Atsushi
3
2018
Relational program reasoning using compiler IR. Zbl 1426.68052
Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias
3
2018
A formalization of metric spaces in HOL Light. Zbl 1425.68376
Maggesi, Marco
2
2018
Toward compositional verification of interruptible OS kernels and device drivers. Zbl 1451.68170
Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui
2
2018
Formalization of the resolution calculus for first-order logic. Zbl 1451.03019
Schlichtkrull, Anders
2
2018
Bidirectional grammars for machine-code decoding and encoding. Zbl 1426.68069
Tan, Gang; Morrisett, Greg
2
2018
A unifying view on SMT-based software verification. Zbl 1426.68041
Beyer, Dirk; Dangl, Matthias; Wendler, Philipp
2
2018
Safe autonomy under perception uncertainty using chance-constrained temporal logic. Zbl 1425.93202
Jha, Susmit; Raman, Vasumathi; Sadigh, Dorsa; Seshia, Sanjit A.
1
2018
Visibly linear temporal logic. Zbl 1425.68182
Bozzelli, Laura; Sánchez, César
1
2018
Many-sorted equivalence of shiny and strongly polite theories. Zbl 1425.68370
Casal, Filipe; Rasga, João
1
2018
OWL reasoning: subsumption test hardness and modularity. Zbl 1398.68518
Matentzoglu, Nicolas; Parsia, Bijan; Sattler, Uli
1
2018
Sentence-normalized conditional narrowing modulo in rewriting logic and Maude. Zbl 1398.68267
Aguirre, Luis; Martí-Oliet, Narciso; Palomino, Miguel; Pita, Isabel
1
2018
CoSMed: a confidentiality-verified social media platform. Zbl 1451.68168
Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco
1
2018
...and 689 more Documents
all top 5

Cited by 4,085 Authors

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

Cited in 219 Journals

468 Journal of Automated Reasoning
199 Artificial Intelligence
181 Theoretical Computer Science
124 Journal of Symbolic Computation
122 Annals of Mathematics and Artificial Intelligence
109 Formalized Mathematics
78 Information and Computation
60 Theory and Practice of Logic Programming
51 MSCS. Mathematical Structures in Computer Science
47 Formal Aspects of Computing
43 Journal of Applied Logic
43 Logical Methods in Computer Science
41 International Journal of Approximate Reasoning
39 Journal of Applied Non-Classical Logics
33 Annals of Pure and Applied Logic
32 Discrete Applied Mathematics
32 Formal Methods in System Design
32 Journal of Logical and Algebraic Methods in Programming
29 Journal of Functional Programming
26 Mathematics in Computer Science
25 Information Processing Letters
23 Constraints
21 Information Sciences
21 Journal of Computer and System Sciences
20 Fuzzy Sets and Systems
20 Studia Logica
18 Applied Mathematics and Computation
18 ACM Transactions on Computational Logic
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 Logica Universalis
11 The Journal of Symbolic Logic
11 The Journal of Logic and Algebraic Programming
10 Journal of Computer Science and Technology
10 Fundamenta Informaticae
9 AI Communications
8 Science of Computer Programming
8 International Journal of Computer Mathematics
8 The Bulletin of Symbolic Logic
7 Journal of Philosophical Logic
7 Notre Dame Journal of Formal Logic
7 JETAI. Journal of Experimental & Theoretical Artificial Intelligence
7 Computational Geometry
7 Journal of Logic, Language and Information
6 International Journal of General Systems
6 Automatica
6 Mathematics and Computers in Simulation
6 Synthese
6 Computers & Operations Research
6 European Journal of Operational Research
6 Soft Computing
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 Machine Learning
5 Archive for Mathematical Logic
5 The Journal of Artificial Intelligence Research (JAIR)
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 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 Journal of Applied Mathematics
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 International Journal of Foundations of Computer Science
3 Cybernetics and Systems Analysis
3 Experimental Mathematics
3 Journal of Heuristics
3 Mathematical Problems in Engineering
3 Journal of Combinatorial Optimization
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 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 Rendiconti dell’Istituto di Matematica dell’Università di Trieste
2 Results in Mathematics
2 Transactions of the American Mathematical Society
2 History and Philosophy of Logic
2 Order
2 Journal of Cryptology
...and 119 more Journals
all top 5

Cited in 52 Fields

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

Citations by Year