default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 52
Volume 52, Number 1, January 2014
- Eugenio G. Omodeo
, Alexandru I. Tomescu:
Set Graphs. III. Proof Pearl: Claw-Free Graphs Mirrored into Transitive Hereditarily Finite Sets. 1-29 - Matthew Gwynne, Oliver Kullmann:
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution. 31-65 - Guido Fiorino:
Terminating Calculi for Propositional Dummett Logic with Subformula Property. 67-97 - Marta R. Hidalgo, Robert Joan-Arinyo:
The Reachability Problem in Constructive Geometric Constraint Solving Based Dynamic Geometry. 99-122
Volume 52, Number 2, February 2014
- Clemens Ballarin:
Locales: A Module System for Mathematical Theories. 123-153 - Temur Kutsia, Jordi Levy, Mateu Villaret:
Anti-unification for Unranked Terms and Hedges. 155-190 - Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban:
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. 191-213 - Jonghyun Park, Jeongbong Seo, Sungwoo Park, Gyesik Lee:
Mechanizing Metatheory Without Typing Contexts. 215-239
Volume 52, Number 3, March 2014
- Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah:
A Framework for the Verification of Certifying Computations. 241-273 - Alexander Malkis, Anindya Banerjee:
On Automation in the Verification of Software Barriers: Experience Report. 275-329 - María-José Hidalgo-Doblado, José A. Alonso-Jiménez, Joaquín Borrego-Díaz, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina:
Formally Verified Tableau-Based Reasoners for a Description Logic. 331-360
Volume 52, Number 4, April 2014
- Mike Stannett, István Németi:
Using Isabelle/HOL to Verify First-Order Relativity Theory. 361-378 - Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun:
Array Theory of Bounded Elements and its Applications. 379-405 - Mark Kaminski, Gert Smolka:
A Goal-Directed Decision Procedure for Hybrid PDL. 407-450 - Chunhan Wu, Xingyuan Zhang, Christian Urban:
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions. 451-480
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-11-22 00:31 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:
