{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T00:30:21Z","timestamp":1768437021929,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540430308","type":"print"},{"value":"9783540453291","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45329-6_31","type":"book-chapter","created":{"date-parts":[[2007,10,25]],"date-time":"2007-10-25T22:44:33Z","timestamp":1193352273000},"page":"306-320","source":"Crossref","is-referenced-by-count":26,"title":["Encodings for Equilibrium Logic and Logic Programs with Nested Expressions"],"prefix":"10.1007","author":[{"given":"David","family":"Pearce","sequence":"first","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,4,23]]},"reference":[{"key":"31_CR1","unstructured":"R. Bayardo and R. Schrag. Using CSP Look-Back Techniques to Solve Real-World SAT Instances. In Proc. AAAI-97, pp. 203\u2013208, 1997."},{"key":"31_CR2","unstructured":"M. Cadoli, A. Giovanardi, and M. Schaerf. An Algorithm to Evaluate Quantified Boolean Formulae. In Proc. AAAI-98, pp. 262\u2013267, 1998."},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"J. Delgrande, T. Schaub, H. Tompits, and S. Woltran. On Computing Solutions to Belief Change Scenarios. In Proc. ECSQARU-01, pp. 510\u2013521, 2001.","DOI":"10.1007\/3-540-44652-4_45"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"E. Eder. Relative Complexities of First-Order Calculi. Vieweg Verlag, 1992.","DOI":"10.1007\/978-3-322-84222-0"},{"key":"31_CR5","unstructured":"U. Egly, T. Eiter, R. Feldmann, V. Klotz, S. Schamberger, H. Tompits, and S. Woltran. On Mechanizing Modal Nonmonotonic Logics. In Proc. DGNMR-01, pp. 44\u201353, 2001."},{"key":"31_CR6","unstructured":"U. Egly, T. Eiter, V. Klotz, H. Tompits, and S. Woltran. Computing Stable Models with Quantified Boolean Formulas: Some Experimental Results. In Proc. AAAI Spring Symposium-01, pp. 53\u201359, 2001."},{"key":"31_CR7","unstructured":"U. Egly, T. Eiter, H. Tompits, and S. Woltran. Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. In Proc. AAAI-00, pp. 417\u2013422, 2000."},{"issue":"3\u20134","key":"31_CR8","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01536399","volume":"15","author":"T. Eiter","year":"1995","unstructured":"T. Eiter and G. Gottlob. On the Computational Cost of Disjunctive Logic Programming: Propositional Case. Ann. of Math. and Artificial Intelligence, 15(3\u20134):289\u2013323, 1995.","journal-title":"Ann. of Math. and Artificial Intelligence"},{"key":"31_CR9","unstructured":"R. Feldmann, B. Monien, and S. Schamberger. A DistributedAlgorithm to Evaluate Quantified Boolean Formulas. In Proc. AAAI-00, pp. 285\u2013290, 2000."},{"key":"31_CR10","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":"31_CR11","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, pp. 364\u2013369, 2001.","DOI":"10.1007\/3-540-45744-5_27"},{"key":"31_CR12","unstructured":"K. G\u00f6del. Zum intuitionistischen Aussagenkalk\u00fcl. Anzeiger der Akademie der Wissenschaften in Wien, pp. 65\u201366, 1932."},{"key":"31_CR13","unstructured":"A. Heyting. Die formalen Regeln der intuitionistischen Logik. Sitz. Berlin, pp. 42\u201356, 1930."},{"key":"31_CR14","unstructured":"H. Kautz and B. Selman. Planning as Satisfiability. In Proc. ECAI-92, pp. 359\u2013363, 1992."},{"issue":"1","key":"31_CR15","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":"31_CR16","unstructured":"R. Letz. Advances in Decision Procedures for Quantified Boolean Formulas. In Proc. IJCAR-01Workshop on Theory and Applications of Quantified Boolean Formulas, pp. 55\u201364, 2001."},{"key":"31_CR17","unstructured":"C. M. Li and Anbulagan. Heuristics Based on Unit Propagation for Satisfiability Problems. In Proc. IJCAI-97, pp. 366\u2013371, 1997."},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"V. Lifschitz, D. Pearce, and A. Valverde. Strongly Equivalent Logic Programs. ACM Transactions on Computational Logic, 2(4), 2001. To appear.","DOI":"10.1145\/383779.383783"},{"issue":"3","key":"31_CR19","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. Ann. of Math. and Artificial Intelligence, 25(3\u20134):369\u2013389, 1999.","journal-title":"Ann. of Math. and Artificial Intelligence"},{"key":"31_CR20","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0743-1066(84)90011-6","volume":"3","author":"J. Lloyd","year":"1984","unstructured":"J. Lloyd and R. Topor. Making Prolog More Expressive. J. of Logic Progr., 3:225\u2013240, 1984.","journal-title":"J. of Logic Progr."},{"key":"31_CR21","first-page":"6","volume":"12","author":"J. Lukasiewicz","year":"1938","unstructured":"J. Lukasiewicz. Die Logik und das Grundlagenproblem. Les Entretiens de Z\u00fcrich sue les Fondements et la M\u00e9thode des Sciences Math\u00e9matiques, 6\u20139, 12 (1938), 1941.","journal-title":"Les Entretiens de Z\u00fcrich sue les Fondements et la M\u00e9thode des Sciences Math\u00e9matiques"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"D. Pearce. A New Logical Characterisation of Stable Models and Answer Sets. In Non-Monotonic Extensions of Logic Programming, pp. 57\u201370. Springer, 1997.","DOI":"10.1007\/BFb0023801"},{"key":"31_CR23","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":"31_CR24","doi-asserted-by":"crossref","unstructured":"D. Pearce, I. de Guzm\u00e1n, and A. Valverde. A Tableau Calculus for Equilibrium Entailment. In Proc. TABLEAUX 2000, pp. 352\u2013367, 2000.","DOI":"10.1007\/10722086_28"},{"key":"31_CR25","doi-asserted-by":"crossref","unstructured":"D. Pearce, I. de Guzm\u00e1n, and A. Valverde. Computing Equilibrium Models Using Signed Formulas. In Proc. Computational Logic 2000, pp. 688\u2013702, 2000.","DOI":"10.1007\/3-540-44957-4_46"},{"issue":"3","key":"31_CR26","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. J. of Symbolic Computation, 2(3):293\u2013304, 1986.","journal-title":"J. of Symbolic Computation"},{"key":"31_CR27","unstructured":"J. Rintanen. Improvements to the Evaluation of Quantified Boolean Formulae. In Proc. IJCAI-99, pp. 1192\u20131197, 1999."},{"key":"31_CR28","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO:An Efficient Propositional Prover. In Proc. CADE-97, pp. 272\u2013275, 1997.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Progress in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45329-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T21:06:26Z","timestamp":1556917586000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45329-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430308","9783540453291"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45329-6_31","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}