![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
Journal of Automated Reasoning (JAR), Volume 40
Volume 40, Number 1, January 2008
- Mark H. Liffiton, Karem A. Sakallah:
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. 1-33 - Jia Meng, Lawrence C. Paulson
:
Translating Higher-Order Clauses to First-Order Clauses. 35-60 - Marc Bezem, Dimitri Hendriks:
On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic. 61-85
Volume 40, Numbers 2-3, March 2008
- Ulrich Furbach:
IJCAR Preface. 87-88 - Yevgeny Kazakov, Boris Motik:
A Resolution-Based Decision Procedure for SHOIQ. 89-116 - David Toman, Grant E. Weddell:
On Keys and Functional Dependencies as First-Class Citizens in Description Logics. 117-132 - Kaustuv Chaudhuri, Frank Pfenning, Greg Price:
A Logical Characterization of Forward and Backward Chaining in the Inverse Method. 133-177 - Andrey Paskevich:
Connection Tableaux with Lazy Paramodulation. 179-194 - Jörg Endrullis
, Johannes Waldmann, Hans Zantema:
Matrix Interpretations for Proving Termination of Term Rewriting. 195-220 - Volker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton:
Automatic Construction and Verification of Isotopy Invariants. 221-243
Volume 40, Number 4, May 2008
- Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore:
A Mechanical Analysis of Program Verification Strategies. 245-269 - Jesús Aransay
, Clemens Ballarin, Julio Rubio
:
A Mechanized Proof of the Basic Perturbation Lemma. 271-292 - Bishop Brock, Matt Kaufmann, J Strother Moore:
Rewriting with Equivalence Relations in ACL2. 293-306 - Laurence Rideau, Bernard P. Serpette, Xavier Leroy:
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves. 307-326 - Christian Urban:
Nominal Techniques in Isabelle/HOL. 327-356 - Yevgeny Kazakov, Boris Motik:
A Resolution-Based Decision Procedure for SHOIQ. 357
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
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.