| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | David Braun, Nicolas Magaud, Pascal Schreck |
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry.  |
J. Autom. Reason.  |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Faissole |
Formally-Verified Round-Off Error Analysis of Runge-Kutta Methods. |
J. Autom. Reason. |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Böhm 0001, Tomás Peitl, Olaf Beyersdorff |
Should Decisions in QCDCL Follow Prefix Order? |
J. Autom. Reason. |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Luca Geatti, Nicola Gigante, Angelo Montanari, Gabriele Venturato |
SAT Meets Tableaux for Linear Temporal Logic Satisfiability. |
J. Autom. Reason. |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominic Steinhöfel, Reiner Hähnle |
Schematic Program Proofs with Abstract Execution. |
J. Autom. Reason. |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Mehdi Mhalla |
A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. |
J. Autom. Reason. |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Bernreiter, Anela Lolic, Jan Maly 0001, Stefan Woltran |
Sequent Calculi for Choice Logics. |
J. Autom. Reason. |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Étienne Payet |
Non-termination in Term Rewriting and Logic Programming. |
J. Autom. Reason. |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Roßkopf, Tobias Nipkow |
A Formalization and Proof Checker for Isabelle's Metalogic. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominik Kirst, Marc Hermes |
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Maximiliano Cristiá, Guido De Luca, Carlos Luna 0001 |
An Automatically Verified Prototype of the Android Permissions System. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Xavier Leroy |
Efficient Extensional Binary Tries. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrei Popescu 0001 |
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic |
Superposition for Higher-Order Logic. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina, Sarah Winkler |
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban |
POSIX Lexing with Derivatives of Regular Expressions. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Mak Andrlon |
Finding Normal Binary Floating-Point Factors Efficiently. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Yun-Rong Luo, Che Cheng, Jie-Hong R. Jiang |
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Emre Yolcu, Scott Aaronson, Marijn J. H. Heule |
An Automated Approach to the Collatz Conjecture. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Guido Fiorino |
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Qinshi Wang, Andrew W. Appel |
A Solver for Arrays with Concatenation. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrzej Indrzejczak |
Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Aaron Windsor |
Computer-Aided Constructions of Commafree Codes. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant |
Preprocessing of Propagation Redundant Clauses. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti |
A Formal Theory of Choreographic Programming. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Alvaro Velasquez, Ismail Alkhouri, K. Subramani 0001, Piotr Wojciechowski 0002, George K. Atia |
Optimal Deterministic Controller Synthesis from Steady-State Distributions. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriel Ebner, Jasmin Blanchette, Sophie Tourret |
Unifying Splitting. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, Cyril Cohen |
Measure Construction by Extension in Dependent Type Theory with Application to Integration. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Anupam Das 0002, Marianna Girlando |
Cyclic Hypersequent System for Transitive Closure Logic. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Nicolas Peltier |
A Proof Procedure for Separation Logic with Inductive Definitions and Data. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Xicheng Peng, Jingzhong Zhang, Mao Chen 0002, Sannyuya Liu |
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds 0001, Cesare Tinelli |
Synthesising Programs with Non-trivial Constants. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Sen Zheng, Renate A. Schmidt |
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Philipp G. Haselwarter, Andrej Bauer |
Finitary Type Theories With and Without Contexts. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar da Silva, Thiago Mendonça Ferreira Ramos |
Formal Verification of Termination Criteria for First-Order Recursive Functions. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Ying Sheng 0007, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds 0001, Clark W. Barrett, Cesare Tinelli |
Combining Stable Infiniteness and (Strong) Politeness. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Karol Pak |
Combining Higher-Order Logic with Set Theory Formalizations. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Hendrik Leidinger, Christoph Weidenbach |
SCL(EQ): SCL for First-Order Logic with Equality. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Oliver Nash |
Engel's Theorem in Mathlib. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux |
Enabling Floating-Point Arithmetic in the Coq Proof Assistant. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson |
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Aart Middeldorp, Alexander Lochmann, Fabian Mitterwallner |
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Marco Maggesi, Cosimo Perini Brogi |
Mechanising Gödel-Löb Provability Logic in HOL Light. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Stepan Holub, Martin Raska, Stepán Starosta |
Binary Codes that do not Preserve Primitivity. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot |
Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Böhm 0001, Olaf Beyersdorff |
Lower Bounds for QCDCL via Formula Gauge. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Pedro Quaresma, Pierluigi Graziani |
Measuring the Readability of Geometric Proofs: The Area Method Case. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Ying Sheng 0007, Andres Nötzli, Andrew Reynolds 0001, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli |
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. |
J. Autom. Reason. |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Sadegh Dalvandi, Brijesh Dongol, Simon Doherty, Heike Wehrheim |
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Joshua Meyers, David I. Spivak, Ryan Wisnesky |
Fast Left Kan Extensions Using the Chase. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Jose Divasón, René Thiemann |
A Formalization of the Smith Normal Form in Higher-Order Logic. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Peltier, Viorica Sofronie-Stokkermans |
Special Issue of Selected Extended Papers of IJCAR 2020. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina |
Six Decades of Automated Reasoning: Papers in Memory of Larry Wos. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon |
Correction to: Local is Best: Efficient Reductions to Modal Logic K. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Piotr Wojciechowski 0002, K. Subramani 0001, R. Chandrasekaran |
Analyzing Read-Once Cutting Plane Proofs in Horn Systems. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Dennis de Champeaux |
Faster Linear Unification Algorithm. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero |
A Coq Formalization of Lebesgue Integration of Nonnegative Functions. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Jose Divasón, René Thiemann |
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
Combination of Uniform Interpolants via Beth Definability. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonathan Julián Huerta y Munive, Georg Struth |
Predicate Transformer Semantics for Hybrid Systems. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Y. Lewis, Minchao Wu |
A Bi-Directional Extensible Interface Between Lean and Mathematica. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Joshua Brakensiek, Marijn Heule, John Mackey, David E. Narváez |
The Resolution of Keller's Conjecture. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette |
A Comprehensive Framework for Saturation Theorem Proving. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Akihisa Yamada 0002 |
Tuple Interpretations for Termination of Term Rewriting. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon |
Local is Best: Efficient Reductions to Modal Logic K. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | David J. Pearce 0001, Mark Utting, Lindsay Groves |
Verifying Whiley Programs with Boogie. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Franz Baader, Jakub Rydval |
Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | André Platzer |
Correction to: Differential Dynamic Logic for Hybrid Systems. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret |
Making Higher-Order Superposition Work. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina |
Set of Support, Demodulation, Paramodulation: A Historical Perspective. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Ying Sheng 0007, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett |
Polite Combination of Algebraic Datatypes. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Franz Baader, Deepak Kapur |
Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Wilmer Ricciotti, James Cheney |
A Formalization of SQL with Nulls. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Veroff |
A Wos Challenge Met. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio |
A Formalization of Dedekind Domains and Class Groups of Global Fields. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar |
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Sarah Sigley, Olaf Beyersdorff |
Proof Complexity of Modal Resolution. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha |
Pardinus: A Temporal Relational Model Finder. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot |
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler |
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Mallku Soldevila, Beta Ziliani, Bruno Silvestre |
From Specification to Testing: Semantics Engineering for Lua 5.2. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Sophie Tourret, Christoph Weidenbach |
A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Thiago Mendonça Ferreira Ramos, Ariane Alves Almeida, Mauricio Ayala-Rincón |
Formalization of the Computational Theory of a Turing Complete Functional Language Model. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe |
Larry Wos: Visions of Automated Reasoning. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Predrag Janicic, Julien Narboux |
Theorem Proving as Constraint Solving with Coherent Logic. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhé Hóu, David Sanán, Alwen Tiu, Yang Liu 0003, Koh Chuen Hoa, Jin Song Dong |
An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Hing-Lun Chan, Michael Norrish |
Mechanisation of the AKS Algorithm. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrei Popescu 0001, Dmitriy Traytel |
Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar |
Automata Terms in a Lazy WSkS Decision Procedure. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Mauro Vallati, Lukás Chrpa, Thomas Leo McCluskey, Frank Hutter |
On the Importance of Domain Model Configuration for Automated Planning Engines. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Xicheng Peng, Qihang Chen, Jingzhong Zhang, Mao Chen 0002 |
Automated Discovery of Geometric Theorems Based on Vector Equations. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | David Butler 0002, Andreas Lochbihler, David Aspinall 0001, Adrià Gascón |
Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Thaynara Arielly de Lima, André Luiz Galdino, Andréia Borges Avelar, Mauricio Ayala-Rincón |
Formalization of Ring Theory in PVS. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Maximiliano Cristiá, Gianfranco Rossi |
An Automatically Verified Prototype of the Tokeneer ID Station Specification. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Pascal Fontaine |
Preface: Special Issue of Selected Extended Papers of CADE 2019. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Blanchette |
Message from the New Editor-in-Chief. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Salvador Lucas |
Derivational Complexity and Context-Sensitive Rewriting. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Yong Guan, Jingzhi Zhang, Guohui Wang, Ximeng Li 0003, Zhiping Shi 0002, Yongdong Li |
Formalization of Euler-Lagrange Equation Set Based on Variational Calculus in HOL Light. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | David M. Cerna, Alexander Leitsch, Anela Lolic |
Schematic Refutations of Formula Schemata. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrei Popescu 0001, Peter Lammich, Ping Hou |
CoCon: A Conference Management System with Formally Verified Document Confidentiality. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license