{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:06:01Z","timestamp":1725483961658},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439301"},{"type":"electronic","value":"9783540456193"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45619-8_28","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:57:41Z","timestamp":1179586661000},"page":"405-420","source":"Crossref","is-referenced-by-count":15,"title":["A Polynomial Translation of Logic Programs with Nested Expressions into Disjunctive Logic Programs: Preliminary Report"],"prefix":"10.1007","author":[{"given":"David","family":"Pearce","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Sarsakov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Torsten","family":"Schaub","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"Tompits","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Woltran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/B978-044450813-3\/50007-2","volume":"I","author":"M. Baaz","year":"2001","unstructured":"M. Baaz, U. Egly, and A. Leitsch. Normal Form Transformations. In Handbook of Automated Reasoning, volume I, chapter 5, pages 273\u2013333. Elsevier Science B. V., 2001.","journal-title":"Handbook of Automated Reasoning"},{"issue":"4","key":"28_CR2","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1006\/jsco.1995.1021","volume":"19","author":"M. Baaz","year":"1995","unstructured":"M. Baaz and C. G. Ferm\u00fcller. Resolution-based Theorem Proving for Many-valued Logics. Journal of Symbolic Computation, 19(4):353\u2013391, 1995.","journal-title":"Journal of Symbolic Computation"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"C. Baral and C. Uyan. Declarative Specification and Solution of Combinatorial Auctions Using Logic Programming. In Proc. LPNMR-01, pages 186\u2013199, 2001.","DOI":"10.1007\/3-540-45402-0_14"},{"key":"28_CR4","unstructured":"M. Cadoli, A. Giovanardi, and M. Schaerf. An Algorithm to Evaluate Quantified Boolean Formulae. In Proc. AAAI-98, pages 262\u2013267, 1998."},{"key":"28_CR5","unstructured":"D. de Jongh and L. Hendriks. Characterization of Strongly Equivalent Logic Programs in Intermediate Logics. Technical report, 2001. Preprint at http:\/\/turing.wins.uva.nl\/~lhendrik\/ ."},{"issue":"2","key":"28_CR6","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1006\/jsco.1996.0044","volume":"22","author":"U. Egly","year":"1996","unstructured":"U. Egly. On Different Structure-Preserving Translations to Normal Form. Journal of Symbolic Computation, 22(2):121\u2013142, 1996.","journal-title":"Journal of Symbolic Computation"},{"issue":"12","key":"28_CR7","doi-asserted-by":"crossref","first-page":"165","DOI":"10.3233\/FI-1997-291208","volume":"29","author":"U. Egly","year":"1997","unstructured":"U. Egly. On Definitional Transformations to Normal Form for Intuitionistic Logic. Fundamenta Informaticae, 29(1,2):165\u2013201, 1997.","journal-title":"Fundamenta Informaticae"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"T. Eiter, N. Leone, C. Mateis, G. Pfeifer, and F. Scarcello. A Deductive System for Non-monotonic Reasoning. In Proc. LPNMR-97, pages 363\u2013374, 1997.","DOI":"10.1007\/3-540-63255-7_27"},{"key":"28_CR9","unstructured":"T. Eiter, N. Leone, C. Mateis, G. Pfeifer, and F. Scarcello. The KR System dlv: Progress Report, Comparisons and Benchmarks. In Proc. KR-98, pages 406\u2013417, 1998."},{"key":"28_CR10","unstructured":"R. Feldmann, B. Monien, and S. Schamberger. A Distributed Algorithm to Evaluate Quantified Boolean Formulas. In Proc. AAAI-00, pages 285\u2013290, 2000."},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"M. Gelfond, M. Balduccini, and J. Galloway. Diagnosing Physical Systems in A-Prolog. In Proc. LPNMR-01, pages 213\u2013225, 2001.","DOI":"10.1007\/3-540-45402-0_16"},{"key":"28_CR12","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/BF03037169","volume":"9","author":"M. Gelfond","year":"1991","unstructured":"M. Gelfond and V. Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9:365\u2013385, 1991.","journal-title":"New Generation Computing"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, M. Narizzano, and A. Tacchella. QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. In Proc. IJCAR-01, pages 364\u2013369, 2001.","DOI":"10.1007\/3-540-45744-5_27"},{"key":"28_CR14","unstructured":"K. G\u00f6del. Zum intuitionistischen Aussagenkalk\u00fcl. Anzeiger der Akademie der Wissenschaften in Wien, pages 65\u201366, 1932."},{"issue":"6","key":"28_CR15","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1093\/logcom\/4.6.905","volume":"4","author":"R. H\u00e4hnle","year":"1994","unstructured":"R. H\u00e4hnle. Short Conjunctive Normal Forms in Finitely Valued Logics. Journal of Logic and Computation, 4(6):905\u2013927, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"K. Heljanko and I. Niemel\u00e4. Bounded LTL Model Checking with Stable Models. In Proc. LPNMR-01, pages 200\u2013212, 2001.","DOI":"10.1007\/3-540-45402-0_15"},{"issue":"1","key":"28_CR17","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0743-1066(97)10001-2","volume":"35","author":"K. Inoue","year":"1998","unstructured":"K. Inoue and C. Sakama. Negation as Failure in the Head. Journal of Logic Programming, 35(1):39\u201378, 1998.","journal-title":"Journal of Logic Programming"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"T. Janhunen. On the Intertranslatability of Autoepistemic, Default and Priority Logics, and Parallel Circumscription. In Proc. JELIA-98, pages 216\u2013232, 1998.","DOI":"10.1007\/3-540-49545-2_15"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"T. Janhunen. On the Effect of Default Negation on the Expressiveness of Disjunctive Rules. In Proc. LPNMR-01, pages 93\u2013106, 2001.","DOI":"10.1007\/3-540-45402-0_7"},{"issue":"1","key":"28_CR20","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine-B\u00fcning","year":"1995","unstructured":"H. Kleine-B\u00fcning, M. Karpinski, and A. Fl\u00f6gel. Resolution for Quantified Boolean Formulas. Information and Computation, 117(1):12\u201318, 1995.","journal-title":"Information and Computation"},{"key":"28_CR21","unstructured":"R. Letz. Advances in Decision Procedures for Quantified Boolean Formulas. In Proc. IJCAR-01 Workshop on Theory and Applications of Quantified Boolean Formulas, pages 55\u201364, 2001."},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"V. Lifschitz. Answer Set Planning. In Proc. ICLP-99, pages 23\u201337, 1999.","DOI":"10.1007\/3-540-46767-X_28"},{"issue":"4","key":"28_CR23","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1145\/383779.383783","volume":"2","author":"V. Lifschitz","year":"2001","unstructured":"V. Lifschitz, D. Pearce, and A. Valverde. Strongly Equivalent Logic Programs. ACM Transactions on Computational Logic, 2(4):526\u2013541, 2001.","journal-title":"ACM Transactions on Computational Logic"},{"issue":"3\u20134","key":"28_CR24","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1023\/A:1018978005636","volume":"25","author":"V. Lifschitz","year":"1999","unstructured":"V. Lifschitz, L. Tang, and H. Turner. Nested Expressions in Logic Programs. Annals of Mathematics and Artificial Intelligence, 25(3\u20134):369\u2013389, 1999.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"28_CR25","unstructured":"F. Lin. Reducing Strong Equivalence of Logic Programs to Entailment in Classical Propositional Logic. In Proc. KR-02, pages 170\u2013176, 2002."},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"G. Mints. Resolution Strategies for the Intuitionistic Logic. In Constraint Programming: NATO ASI Series, pages 282\u2013304. Springer, 1994.","DOI":"10.1007\/978-3-642-85983-0_11"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"I. Niemel\u00e4 and P. Simons. Smodels: An Implementation of the Stable Model and Well-Founded Semantics for Normal Logic Programs. In Proc. LPNMR-97, pages 420\u2013429, 1997.","DOI":"10.1007\/3-540-63255-7_32"},{"key":"28_CR28","doi-asserted-by":"crossref","unstructured":"D. Pearce. A New Logical Characterisation of Stable Models and Answer Sets. In Non-Monotonic Extensions of Logic Programming, pages 57\u201370. Springer, 1997.","DOI":"10.1007\/BFb0023801"},{"key":"28_CR29","doi-asserted-by":"crossref","unstructured":"D. Pearce. From Here to There: Stable Negation in Logic Programming. In What is Negation? Kluwer, 1999.","DOI":"10.1007\/978-94-015-9309-0_8"},{"key":"28_CR30","doi-asserted-by":"crossref","unstructured":"D. Pearce, I. de Guzm\u00e1n, and A. Valverde. A Tableau Calculus for Equilibrium Entailment. In Proc. TABLEAUX-00, pages 352\u2013367, 2000.","DOI":"10.1007\/10722086_28"},{"key":"28_CR31","doi-asserted-by":"crossref","unstructured":"D. Pearce, I. de Guzm\u00e1n, and A. Valverde. Computing Equilibrium Models Using Signed Formulas. In Proc. CL-00, pages 688\u2013702, 2000.","DOI":"10.1007\/3-540-44957-4_46"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"D. Pearce, H. Tompits, and S. Woltran. Encodings for Equilibrium Logic and Logic Programs with Nested Expressions. In Proc. EPIA-01, pages 306\u2013320. Springer, 2001.","DOI":"10.1007\/3-540-45329-6_31"},{"issue":"3","key":"28_CR33","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"D. A. Plaisted and S. Greenbaum. A Structure Preserving Clause Form Translation. Journal of Symbolic Computation, 2(3):293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"28_CR34","unstructured":"J. Rintanen. Improvements to the Evaluation of Quantified Boolean Formulae. In Proc. IJCAI-99, pages 1192\u20131197, 1999."},{"key":"28_CR35","doi-asserted-by":"crossref","unstructured":"J. Siekmann and G. Wrightson, editors. Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, volume 2. Springer-Verlag, 1983.","DOI":"10.1007\/978-3-642-81955-1"},{"key":"28_CR36","doi-asserted-by":"crossref","unstructured":"G. Tseitin. On the Complexity of Proofs in Propositional Logics. Seminars in Mathematics, 8, 1970. Reprinted in [35].","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45619-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T05:20:31Z","timestamp":1587532831000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45619-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439301","9783540456193"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-45619-8_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}