Logic for Programming, Artificial Intelligence, and Reasoning | Zendy

Jaime Carbonell | Zendy; Jörg Siekmann | Zendy; Miki Hermann | Zendy; Андрей Воронков | Zendy; Workshop Chair | Zendy; Christelle Scharff | Zendy; Marı́a Alpuente | Zendy; Franz Baader | Zendy; Matthias Baaz | Zendy; Christoph Benzmüller | Zendy; Koen Claessen | Zendy; Javier Esparza | Zendy; Bernd Fischer | Zendy; Jürgen Giesl | Zendy; Jean Goubault-Larrecq | Zendy; Erich Grädel | Zendy; Ziyad Hanna | Zendy; Pascal Van Hentenryck | Zendy; Brahim Hnich | Zendy; Ian Horrocks | Zendy; Viktor Kunčak | Zendy; Orna Kupferman | Zendy; Christopher J. Lynch | Zendy; Dale Miller | Zendy; George C. Necula | Zendy; Joachim Niehren | Zendy; C.-H. Luke Ong | Zendy; Catuscia Palamidessi | Zendy; Michel Parigot | Zendy; Frank Pfenning | Zendy; Reinhard Pichler | Zendy; Michaël Rusinowitch | Zendy; Mooly Sagiv | Zendy; Gernot Salzer | Zendy; Sopheap Seng | Zendy; Geoff Sutcliffe | Zendy; Sophie Tison | Zendy; Margus Veanes | Zendy; Alicia Villanueva | Zendy; David D. Fang | Zendy; W K Hung Benjamin | Zendy; Werner Wies | Zendy; Stefan Woltran | Zendy; James Worrell | Zendy; Hongwei Xi | Zendy; Avi Yadgar | Zendy; Greta Yorsh | Zendy; Karen Zee | Zendy; Juergen Zimmer | Zendy; Evgeny Zolin | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Logic for Programming, Artificial Intelligence, and Reasoning

Author(s) -

Jaime Carbonell,

Jörg Siekmann,

Miki Hermann,

Андрей Воронков,

Workshop Chair,

Christelle Scharff,

Marı́a Alpuente,

Franz Baader,

Matthias Baaz,

Christoph Benzmüller,

Koen Claessen,

Javier Esparza,

Bernd Fischer,

Jürgen Giesl,

Jean Goubault-Larrecq,

Erich Grädel,

Ziyad Hanna,

Pascal Van Hentenryck,

Brahim Hnich,

Ian Horrocks,

Viktor Kunčak,

Orna Kupferman,

Christopher J. Lynch,

Dale Miller,

George C. Necula,

Joachim Niehren,

C.-H. Luke Ong,

Catuscia Palamidessi,

Michel Parigot,

Frank Pfenning,

Reinhard Pichler,

Michaël Rusinowitch,

Mooly Sagiv,

Gernot Salzer,

Sopheap Seng,

Geoff Sutcliffe,

Sophie Tison,

Margus Veanes,

Alicia Villanueva,

David D. Fang,

W K Hung Benjamin,

Werner Wies,

Stefan Woltran,

James Worrell,

Hongwei Xi,

Avi Yadgar,

Greta Yorsh,

Karen Zee,

Juergen Zimmer,

Evgeny Zolin

Publication year - 2006

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

eISSN - 1611-3349

pISSN - 0302-9743

DOI - 10.1007/11916277

Subject(s) - computer science , logic programming , programming language , automated reasoning , artificial intelligence , cognitive science , psychology

We address the problems of combining satisfiability procedures and consider two combination scenarios: (i) the combination within the class of rewriting-based satisfiability procedures and (ii) the Nelson-Oppen combination of rewriting-based satisfiability procedures and arbitrary satisfiability procedures. In each scenario, we use meta-saturation, which schematizes saturation of the set containing the axioms of a given theory and an arbitrary set of ground literals, to syntactically decide sufficient conditions for the combinability of rewriting-based satisfiability procedures. For (i), we give a sufficient condition for the modular termination of meta-saturation. When meta-saturation for the union of theories halts, it yields a rewriting-based satisfiability procedure for the union. For (ii), we use meta-saturation to prove the stable infiniteness of the component theories and deduction completeness of their rewriting-based satisfiability procedures. These properties are important to establish the correctness of the Nelson-Oppen combination method and to obtain an efficient implementation

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research