http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
이 학술지의 논문 검색
Encoding RTL Constructs for MathSAT: a Preliminary Report
Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Franzen, A.; Hanna, Z.; Khasidashvili, Z.; Palti, A.; Sebastiani, R. ELSEVIER SCIENCE B.V AMSTERDAM 2006 p.3-14
Tool Building Requirements for an API to First-Order Solvers
Grundy, J.; Melham, T.; Krstic, S.; McLaughlin, S. ELSEVIER SCIENCE B.V AMSTERDAM 2006 p.15-26
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Lahiri, S. K.; Musuvathi, M. ELSEVIER SCIENCE B.V AMSTERDAM 2006 p.27-41
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite
McLaughlin, S.; Barrett, C.; Ge, Y. ELSEVIER SCIENCE B.V AMSTERDAM 2006 p.43-51
Reduced Functional Consistency of Uninterpreted Functions
Pnueli, A.; Strichman, O. ELSEVIER SCIENCE B.V AMSTERDAM 2006 p.53-65
Integrating a SAT Solver with an LCF-style Theorem Prover
Weber, T. ELSEVIER SCIENCE B.V AMSTERDAM 2006 p.67-78
Mining Propositional Simplification Proofs for Small Validating Clauses
Wehrman, I.; Stump, A. ELSEVIER SCIENCE B.V AMSTERDAM 2006 p.79-91