default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 68
Volume 68, Number 1, March 2024
- Florian Faissole
:
Formally-Verified Round-Off Error Analysis of Runge-Kutta Methods. 1 - Mnacho Echenim, Mehdi Mhalla:
A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. 2 - David Braun, Nicolas Magaud, Pascal Schreck:
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry. 3 - Étienne Payet:
Non-termination in Term Rewriting and Logic Programming. 4 - Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff:
Should Decisions in QCDCL Follow Prefix Order? 5
Volume 68, Number 2, June 2024
- Luca Geatti, Nicola Gigante, Angelo Montanari, Gabriele Venturato:
SAT Meets Tableaux for Linear Temporal Logic Satisfiability. 6 - Dominic Steinhöfel, Reiner Hähnle:
Schematic Program Proofs with Abstract Execution. 7 - Michael Bernreiter, Anela Lolic, Jan Maly, Stefan Woltran:
Sequent Calculi for Choice Logics. 8 - Filip Smola, Jacques D. Fleuriot:
Linear Resources in Isabelle/HOL. 9 - Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth:
Formalized Functional Analysis with Semilinear Maps. 10 - Lei Li, Zongkai Yang, Mao Chen, Xicheng Peng, Jianwen Sun, Zhonghua Yan, Sannyuya Liu:
Automated Generation of Geometry Proof Problems Based on Point Geometry Identity. 11 - Tobias Nipkow:
Gale-Shapley Verified. 12
Volume 68, Number 3, September 2024
- Camillo Fiorentini, Mauro Ferrari:
General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic. 13 - Peter Lammich:
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting. 14 - Asta Halkjær From, Frederik Krogsdal Jacobsen:
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. 15 - Abhimanyu Choudhury, Meena Mahajan:
Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study. 16 - Guy Amir, Osher Maayan, Tom Zelazny, Guy Katz, Michael Schapira:
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains. 17 - Zhongye Wang, Qinxiang Cao, Yichen Tao:
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding. 18 - Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala:
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. 19
Volume 68, Number 4, December 2024
- Philippe Malbos, Tanguy Massacrier, Georg Struth:
Single-Set Cubical Categories and Their Formalisation with a Proof Assistant. 20 - Jonathan Julián Huerta y Munive, Simon Foster, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen, Thomas Hickman:
IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale. 21 - Hing-Lun Chan:
Windmills of the Minds: A Hopping Algorithm for Fermat's Two Squares Theorem. 22 - Maximiliano Cristiá, Gianfranco Rossi:
A Practical Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers. 23 - Christoph Wernhard, Wolfgang Bibel:
Investigations into Proof Structures. 24 - Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, Daniele Nantes-Sobrinho:
Certified First-Order AC-Unification and Applications. 25
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-02-15 00:21 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
