Boris Konev / Frank Wolter (eds.)

Frontiers of Combining Systems

6th International Symposium, FroCoS 2007, Liverpool, UK, September 10-12, 2007. Proceedings
Herausgegeben:Konev, Boris; Wolter, Frank

• Broschiertes Buch

Produktbeschreibung

Section 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.

Produktdetails

• Lecture Notes in Computer Science 4720
• Verlag: Springer / Springer Berlin Heidelberg / Springer, Berlin
• Artikelnr. des Verlages: 12115235, 978-3-540-74620-1
• Seitenzahl: 296
• Erscheinungstermin: 23. August 2007
• Englisch
• Abmessung: 235mm x 155mm x 17mm
• Gewicht: 457g
• ISBN-13: 9783540746201
• ISBN-10: 354074620X
• Artikelnr.: 23113070

Inhaltsangabe

Section 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.