default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 67
Volume 67, Number 1, March 2023
- Simon Roßkopf
, Tobias Nipkow:
A Formalization and Proof Checker for Isabelle's Metalogic. 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. 2 - Guido Fiorino:
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic. 3 - Qinshi Wang, Andrew W. Appel:
A Solver for Arrays with Concatenation. 4 - Pedro Quaresma, Pierluigi Graziani:
Measuring the Readability of Geometric Proofs: The Area Method Case. 5 - Maria Paola Bonacina, Sarah Winkler:
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover. 6 - Alvaro Velasquez, Ismail Alkhouri, K. Subramani, Piotr Wojciechowski, George K. Atia:
Optimal Deterministic Controller Synthesis from Steady-State Distributions. 7 - Andrew W. Appel, Xavier Leroy:
Efficient Extensional Binary Tries. 8 - Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot:
Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. 9 - Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic:
Superposition for Higher-Order Logic. 10 - Mak Andrlon:
Finding Normal Binary Floating-Point Factors Efficiently. 11 - Aaron Windsor:
Computer-Aided Constructions of Commafree Codes. 12 - Dominik Kirst, Marc Hermes:
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. 13
Volume 67, Number 2, June 2023
- Aart Middeldorp, Alexander Lochmann, Fabian Mitterwallner:
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification. 14 - Emre Yolcu, Scott Aaronson, Marijn J. H. Heule:
An Automated Approach to the Collatz Conjecture. 15 - Gabriel Ebner, Jasmin Blanchette, Sophie Tourret:
Unifying Splitting. 16 - Maximiliano Cristiá, Guido De Luca, Carlos Luna:
An Automatically Verified Prototype of the Android Permissions System. 17 - Oliver Nash:
Engel's Theorem in Mathlib. 18 - Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli:
Synthesising Programs with Non-trivial Constants. 19 - Cezary Kaliszyk, Karol Pak:
Combining Higher-Order Logic with Set Theory Formalizations. 20 - Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti:
A Formal Theory of Choreographic Programming. 21
Volume 67, Number 3, September 2023
- Hendrik Leidinger, Christoph Weidenbach:
SCL(EQ): SCL for First-Order Logic with Equality. 22 - Andrei Popescu:
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version. 23 - Christian Urban:
POSIX Lexing with Derivatives of Regular Expressions. 24 - Stepan Holub, Martin Raska, Stepán Starosta:
Binary Codes that do not Preserve Primitivity. 25 - Yun-Rong Luo, Che Cheng, Jie-Hong R. Jiang:
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability. 26 - Anupam Das, Marianna Girlando:
Cyclic Hypersequent System for Transitive Closure Logic. 27 - Reynald Affeldt, Cyril Cohen:
Measure Construction by Extension in Dependent Type Theory with Application to Integration. 28 - Marco Maggesi, Cosimo Perini Brogi:
Mechanising Gödel-Löb Provability Logic in HOL Light. 29 - Mnacho Echenim, Nicolas Peltier:
A Proof Procedure for Separation Logic with Inductive Definitions and Data. 30 - Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Preprocessing of Propagation Redundant Clauses. 31 - Ying Sheng, Andres Nötzli, Andrew Reynolds, 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. 32
Volume 67, Number 4, December 2023
- Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux:
Enabling Floating-Point Arithmetic in the Coq Proof Assistant. 33 - Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Combining Stable Infiniteness and (Strong) Politeness. 34 - Benjamin Böhm, Olaf Beyersdorff:
Lower Bounds for QCDCL via Formula Gauge. 35 - Philipp G. Haselwarter, Andrej Bauer:
Finitary Type Theories With and Without Contexts. 36 - Andrzej Indrzejczak:
Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation. 37 - Xicheng Peng, Jingzhong Zhang, Mao Chen, Sannyuya Liu:
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity. 38 - Sen Zheng, Renate A. Schmidt:
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments. 39 - 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. 40
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 2024-12-04 20:19 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:
