![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
3rd PDPAR@CAV 2005: Edinburgh, UK
- Alessandro Armando, Alessandro Cimatti:
Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, PDPAR@CAV 2005, Edinburgh, UK, July 12, 2005. Electronic Notes in Theoretical Computer Science 144(2), Elsevier 2006 - Alessandro Armando
, Alessandro Cimatti
:
Preface. 1-2 - Marco Bozzano
, Roberto Bruttomesso, Alessandro Cimatti
, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani:
Encoding RTL Constructs for MathSAT: a Preliminary Report. 3-14 - Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin:
Tool Building Requirements for an API to First-Order Solvers. 15-26 - Shuvendu K. Lahiri, Madanlal Musuvathi:
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals. 27-41 - Sean McLaughlin, Clark W. Barrett
, Yeting Ge:
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. 43-51 - Amir Pnueli, Ofer Strichman
:
Reduced Functional Consistency of Uninterpreted Functions. 53-65 - Tjark Weber:
Integrating a SAT Solver with an LCF-style Theorem Prover. 67-78 - Ian Wehrman, Aaron Stump:
Mining Propositional Simplification Proofs for Small Validating Clauses. 79-91
![](https://dblp.uni-trier.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.