LEADER 03095oam  2200589   450 
001 996465926103316
005 20210521080807.0
010   $a3-540-74621-8
024 7 $a10.1007/978-3-540-74621-8
035   $a(CKB)1000000000490595
035   $a(SSID)ssj0000317808
035   $a(PQKBManifestationID)11230713
035   $a(PQKBTitleCode)TC0000317808
035   $a(PQKBWorkID)10295541
035   $a(PQKB)11652150
035   $a(DE-He213)978-3-540-74621-8
035   $a(MiAaPQ)EBC3063305
035   $a(MiAaPQ)EBC6413303
035   $a(PPN)123164745
035   $a(EXLCZ)991000000000490595
100   $a20210521d2007      uy             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 00$aFrontiers of combining systems $e6th international symposium, frocos 2007, liverpool, uk, september 10-12, 2007. Proceedings /$fedited by Boris Konev, Frank Wolter
205   $a1st ed. 2007.
210  1$aBerlin, Germany ;$aNew York, United States :$cSpringer,$d[2007]
210  4$d©2007
215   $a1 online resource (X, 286 p.) 
225 1 $aLecture notes in computer science. Lecture notes in artificial intelligence ; 4720,$x0302-9743
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-74620-X 
320   $aIncludes bibliographical references and index.
327   $aSection 1. Invited Contributions -- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL -- From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain -- Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions -- Temporalising Logics: Fifteen Years After -- Section 2. Technical Papers -- Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs -- A Compressing Translation from Propositional Resolution to Natural Deduction -- Combining Algorithms for Deciding Knowledge in Security Protocols -- Combining Classical and Intuitionistic Implications -- Towards an Automatic Analysis of Web Service Security -- Certification of Automated Termination Proofs -- Temporal Logic with Capacity Constraints -- Idempotent Transductions for Modal Logics -- A Temporal Logic of Robustness -- Noetherianity and Combination Problems -- Languages Modulo Normalization -- Combining Proof-Producing Decision Procedures -- Visibly Pushdown Languages and Term Rewriting -- Proving Termination Using Recursive Path Orders and SAT Solving.
410  0$aLecture notes in computer science.$pLecture notes in artificial intelligence ;$v4720.
517 3 $aFroCos 2007
606   $aComputer science$vCongresses
606   $aLogic, Symbolic and mathematical$vCongresses
615  0$aComputer science
615  0$aLogic, Symbolic and mathematical
676   $a511.3
702   $aKonev$b Boris
702   $aWolter$b Frank
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bUtOrBLW
906   $aBOOK
912   $a996465926103316
996   $aFrontiers of Combining Systems$92555154
997   $aUNISA