{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,26]],"date-time":"2026-01-26T15:32:58Z","timestamp":1769441578548,"version":"3.49.0"},"reference-count":80,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2000,11,1]],"date-time":"2000-11-01T00:00:00Z","timestamp":973036800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T00:00:00Z","timestamp":1374710400000},"content-version":"vor","delay-in-days":4649,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[2000,11]]},"DOI":"10.1016\/s0004-3702(00)00070-9","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T14:41:58Z","timestamp":1027608118000},"page":"87-138","source":"Crossref","is-referenced-by-count":62,"title":["EXPtime tableaux for ALC"],"prefix":"10.1016","volume":"124","author":[{"given":"Francesco M.","family":"Donini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Massacci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S0004-3702(00)00070-9_ID007","doi-asserted-by":"crossref","first-page":"706","DOI":"10.1145\/155183.155225","article-title":"A calculus for access control in distributed systems","volume":"Vol. 15","author":"Abadi","year":"1993","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"10.1016\/S0004-3702(00)00070-9_ID008","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0304-3975(95)00193-X","article-title":"A proper hierarchy of propositional sequent calculi","volume":"Vol. 159","author":"Arai","year":"1996","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"10.1016\/S0004-3702(00)00070-9_ID009","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BF00872105","article-title":"An empirical analysis of optimization techniques for terminological representation systems or: \u201cmaking KRIS get a move on\u201d","volume":"Vol. 4","author":"Baader","year":"1994","journal-title":"Appl. Intelligence"},{"key":"10.1016\/S0004-3702(00)00070-9_ID010","series-title":"Proc. 5th Kurt G\u00f6del Colloquium, KGC'97","first-page":"89","article-title":"A new method for bounding the complexity of modal logics","volume":"Vol. 1289","author":"Basin","year":"1997"},{"key":"10.1016\/S0004-3702(00)00070-9_ID011","series-title":"Proc. 5th European Workshop on Logics in Artificial Intelligence (JELIA'96)","first-page":"1","article-title":"Hyper tableaux","volume":"Vol. 1126","author":"Baumgartner","year":"1996"},{"key":"10.1016\/S0004-3702(00)00070-9_ID012","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/BF01050635","article-title":"A modal perspective on computational complexity of attribute value grammar","volume":"Vol. 2","author":"Blackburn","year":"1993","journal-title":"J. Logic Language and Inform."},{"key":"10.1016\/S0004-3702(00)00070-9_ID013","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1613\/jair.56","article-title":"A semantics and complete algorithm for subsumption in the CLASSIC description logic","volume":"Vol. 1","author":"Borgida","year":"1994","journal-title":"J. Artificial Intelligence Res."},{"key":"10.1016\/S0004-3702(00)00070-9_ID014","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1613\/jair.21","article-title":"Decidable reasoning in terminological knowledge representation systems","volume":"Vol. 1","author":"Buchheit","year":"1993","journal-title":"J. Artificial Intelligence Res."},{"key":"10.1016\/S0004-3702(00)00070-9_ID015","series-title":"Proc. AAAI-98, Madison, WI","first-page":"205","article-title":"What can knowledge representation do for semi-structured data?","author":"Calvanese","year":"1998"},{"key":"10.1016\/S0004-3702(00)00070-9_ID016","series-title":"Proc. 6th International Conference on Principles of Knowledge Representation and Reasoning (KR-98), Trento, Italy","first-page":"2","article-title":"Description logic framework for information integration","author":"Calvanese","year":"1998"},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID017","doi-asserted-by":"crossref","first-page":"281","DOI":"10.3233\/FI-1997-323404","article-title":"Modal tableaux with propagation rules and structural rules","volume":"Vol. 32","author":"Castilho","year":"1997","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S0004-3702(00)00070-9_ID018","series-title":"Proc. International Conference on Analytic Tableaux and Related Methods (TABLEAUX'97)","first-page":"138","article-title":"Hintikka multiplicities in matrix decision methods for some propositional modal logics","volume":"Vol. 1227","author":"Cerrito","year":"1997"},{"key":"10.1016\/S0004-3702(00)00070-9_ID019","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","article-title":"Memory efficient algorithms for the verification of temporal properties","volume":"Vol. 1","author":"Courcoubetis","year":"1992","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S0004-3702(00)00070-9_ID020","series-title":"Proc. 5th International Conference on the Principles of Knowledge Representation and Reasoning (KR-96), Cambridge, MA","first-page":"316","article-title":"Tbox and abox reasoning in expressive description logics","author":"De Giacomo","year":"1996"},{"key":"10.1016\/S0004-3702(00)00070-9_ID021","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1613\/jair.334","article-title":"A uniform framework for concept definitions in description logics","volume":"Vol. 6","author":"De Giacomo","year":"1997","journal-title":"J. Artificial Intelligence Res."},{"key":"10.1016\/S0004-3702(00)00070-9_ID022","unstructured":"G. De Giacomo, F. Massacci, Combining deduction and model checking into tableaux and algorithms for Converse-PDL, to appear in Information and Computation (accepted in 1997). An online version is at http:\/\/www.academicpress.com\/i&c on IDEALfirst. A preliminary version appeared in: Proc. CADE-96, Lecture Notes in Artificial Intelligence, Vol. 1104, 1996, Springer, Berlin, pp. 613\u2013628"},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID023","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0004-3702(90)90046-3","article-title":"Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition","volume":"Vol. 41","author":"Dechter","year":"1990","journal-title":"Artificial Intelligence"},{"issue":"1","key":"10.1016\/S0004-3702(00)00070-9_ID024","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1080\/11663081.1995.10510844","article-title":"Uniform and non uniform strategies for tableaux calculi for modal logics","volume":"Vol. 5","author":"Demri","year":"1995","journal-title":"J. Appl. Non-Classical Logics"},{"issue":"5","key":"10.1016\/S0004-3702(00)00070-9_ID025","first-page":"36","article-title":"LASSIE: A knowledge-based software information system","volume":"Vol. 34","author":"Devambu","year":"1991","journal-title":"Comm. ACM"},{"key":"10.1016\/S0004-3702(00)00070-9_ID026","series-title":"Proc. 1996 Description Logic Workshop (DL-96)","first-page":"107","article-title":"EXPTIME tableaux for ALC","author":"Donini","year":"1996"},{"key":"10.1016\/S0004-3702(00)00070-9_ID027","series-title":"Proc. IJCAI-91, Sydney, Australia","first-page":"458","article-title":"Tractable concept languages","author":"Donini","year":"1991"},{"key":"10.1016\/S0004-3702(00)00070-9_ID028","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1997.2625","article-title":"The complexity of concept languages","volume":"Vol. 134","author":"Donini","year":"1997","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0004-3702(00)00070-9_ID029","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/0004-3702(91)90029-J","article-title":"Two theses of knowledge representation: Language restrictions, taxonomic classification, and the utility of representation services","volume":"Vol. 48","author":"Doyle","year":"1991","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0004-3702(00)00070-9_ID030","series-title":"Logics for Concurrency (Structure versus Automata)","first-page":"41","article-title":"Automated temporal reasoning about reactive systems","volume":"Vol. 1043","author":"Emerson","year":"1996"},{"key":"10.1016\/S0004-3702(00)00070-9_ID031","series-title":"Reasoning about Knowledge","author":"Fagin","year":"1995"},{"issue":"4","key":"10.1016\/S0004-3702(00)00070-9_ID032","doi-asserted-by":"crossref","first-page":"317","DOI":"10.3233\/FI-1999-40401","article-title":"Tableaux based decision procedures for modal logics of confluence and density","volume":"Vol. 40","author":"Fari\u00f1as del Cerro","year":"1999","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S0004-3702(00)00070-9_ID033","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"Vol. 18","author":"Fischer","year":"1979","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0004-3702(00)00070-9_ID034","series-title":"Proof Methods for Modal and Intuitionistic Logics","author":"Fitting","year":"1983"},{"key":"10.1016\/S0004-3702(00)00070-9_ID035","series-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1","first-page":"365","article-title":"Basic modal logic","author":"Fitting","year":"1993"},{"key":"10.1016\/S0004-3702(00)00070-9_ID036","series-title":"Proc. 1998 Internat. Workshop on Description Logics","year":"1998"},{"key":"10.1016\/S0004-3702(00)00070-9_ID037","series-title":"Protocol Specification Testing and Verification (PSVT-95), Warsaw, Poland","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic","author":"Gerth","year":"1995"},{"issue":"2","key":"10.1016\/S0004-3702(00)00070-9_ID038","doi-asserted-by":"crossref","DOI":"10.1080\/11663081.2000.10510994","article-title":"SAT vs. translation based decision procedures for modal logics: A comparative evaluation","volume":"Vol. 10","author":"Giunchiglia","year":"2000","journal-title":"J. Appl. Non-Classical Logics"},{"key":"10.1016\/S0004-3702(00)00070-9_ID039","series-title":"Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000)","article-title":"A subset-matching size-bounded cache for satisfiability in modal logics","volume":"Vol. 1847","author":"Giunchiglia","year":"2000"},{"key":"10.1016\/S0004-3702(00)00070-9_ID040","series-title":"Proc. 13th International Conference on Automated Deduction (CADE'96)","first-page":"583","article-title":"Building decision procedures for modal logics from propositional decision procedures\u2014The case study of modal K","volume":"Vol. 1104","author":"Giunchiglia","year":"1996"},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID041","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1145\/146937.146940","article-title":"A logic for reasoning about security","volume":"Vol. 10","author":"Glasgow","year":"1992","journal-title":"ACM Trans. Comput. Syst."},{"key":"10.1016\/S0004-3702(00)00070-9_ID042","series-title":"Handbook of Tableau Methods","article-title":"Tableau methods for modal and temporal logics","author":"Gor\u00e9","year":"1999"},{"key":"10.1016\/S0004-3702(00)00070-9_ID043","series-title":"Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000)","article-title":"Consistency testing: The RACE experience","volume":"Vol. 1847","author":"Haarslev","year":"2000"},{"key":"10.1016\/S0004-3702(00)00070-9_ID044","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","article-title":"A guide to completeness and complexity for modal logics of knowledge and belief","volume":"Vol. 54","author":"Halpern","year":"1992","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0004-3702(00)00070-9_ID045","series-title":"Proc. 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'96)","first-page":"210","article-title":"Efficient loop-check for backward proof search in some non-classical logics","volume":"Vol. 1071","author":"Heuerding","year":"1996"},{"key":"10.1016\/S0004-3702(00)00070-9_ID046","series-title":"Proc. IJCAI-99, Stockholm, Sweden","first-page":"462","article-title":"A new method to index and query sets","author":"Hoffman","year":"1999"},{"key":"10.1016\/S0004-3702(00)00070-9_ID047","series-title":"Proc. 6th International Conference on Principles of Knowledge Representation and Reasoning (KR-98), Trento, Italy","first-page":"636","article-title":"Using an expressive description logic: FaCT or fiction?","author":"Horrocks","year":"1998"},{"key":"10.1016\/S0004-3702(00)00070-9_ID048","series-title":"Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000)","first-page":"62","article-title":"Benchmark analysis with FaCT","volume":"Vol. 1847","author":"Horrocks","year":"2000"},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID049","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","article-title":"Optimizing description logic subsumption","volume":"Vol. 9","author":"Horrocks","year":"1999","journal-title":"J. Logic Comput."},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID050","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1093\/logcom\/9.3.385","article-title":"A description logic with transitive and inverse roles and role hierarchies","volume":"Vol. 9","author":"Horrocks","year":"1999","journal-title":"J. Logic Comput."},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID051","first-page":"239","article-title":"Practical reasoning for expressive description logics","volume":"Vol. 8","author":"Horrocks","year":"2000","journal-title":"J. Interest Group in Pure and Applied Logic"},{"key":"10.1016\/S0004-3702(00)00070-9_ID052","series-title":"Proc. 7th International Conference on Principles of Knowledge Representation and Reasoning (KR'2000), Breckenridge, CO","first-page":"285","article-title":"Reasoning with axioms: Theory and practice","author":"Horrocks","year":"2000"},{"key":"10.1016\/S0004-3702(00)00070-9_ID053","series-title":"Proc. IJCAI-99, Stockholm, Sweden","first-page":"110","article-title":"On the relation of resolution and tableaux proof systems for description logics","author":"Hustadt","year":"1999"},{"issue":"4","key":"10.1016\/S0004-3702(00)00070-9_ID054","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1080\/11663081.1999.10510981","article-title":"An empirical analysis of modal theorem provers","volume":"Vol. 9","author":"Hustadt","year":"1999","journal-title":"J. Appl. Non-Classical Logics"},{"key":"10.1016\/S0004-3702(00)00070-9_ID055","series-title":"Handbook of Theoretical Computer Science, Vol. II","article-title":"Logic of programs","author":"Kozen","year":"1990"},{"key":"10.1016\/S0004-3702(00)00070-9_ID056","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","article-title":"Semantical analysis of modal logic I: Normal propositional calculi","volume":"Vol. 9","author":"Kripke","year":"1963","journal-title":"Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik"},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID057","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","article-title":"The computational complexity of provability in systems of modal propositional logic","volume":"Vol. 6","author":"Ladner","year":"1977","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0004-3702(00)00070-9_ID058","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0004-3702(84)90009-2","article-title":"Foundations of a functional approach to knowledge representation","volume":"Vol. 23","author":"Levesque","year":"1984","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0004-3702(00)00070-9_ID059","series-title":"Readings in Knowledge Representation","first-page":"41","article-title":"A fundamental tradeoff in knowledge representation and reasoning","author":"Levesque","year":"1985"},{"key":"10.1016\/S0004-3702(00)00070-9_ID060","series-title":"Proc. 12th International Conference on Automated Deduction (CADE'94)","first-page":"723","article-title":"Strongly analytic tableaux for normal modal logics","volume":"Vol. 814","author":"Massacci","year":"1994"},{"key":"10.1016\/S0004-3702(00)00070-9_ID061","series-title":"Proc. 2nd International Conference on Analytic Tableaux and Related Methods (TABLEAUX'98)","first-page":"217","article-title":"Simplification: A general constraint propagation technique for propositional and modal tableaux","volume":"Vol. 1397","author":"Massacci","year":"1998"},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID062","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1093\/logcom\/8.3.373","article-title":"Tableaux methods for formal verification in multi-agent distributed systems","volume":"Vol. 8","author":"Massacci","year":"1998","journal-title":"J. Logic Comput."},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID063","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1023\/A:1006155811656","article-title":"Single step tableaux for modal logics: Methodology, computations, algorithms","volume":"Vol. 24","author":"Massacci","year":"2000","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0004-3702(00)00070-9_ID064","series-title":"Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000)","article-title":"Design and results of TANCS-00","volume":"Vol. 1847","author":"Massacci","year":"2000"},{"key":"10.1016\/S0004-3702(00)00070-9_ID065","series-title":"The LEDA User Manual, http:\/\/www.mpi-sb.mpg.de\/LEDA\/","author":"Mehlhorn","year":"1998"},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID066","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/0004-3702(88)90066-5","article-title":"Computational complexity of terminological reasoning in BACK","volume":"Vol. 34","author":"Nebel","year":"1988","journal-title":"Artificial Intelligence"},{"issue":"1","key":"10.1016\/S0004-3702(00)00070-9_ID067","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/200836.200848","article-title":"Reasoning about temporal relations: A maximal tractable subclass of Allen's interval algebra","volume":"Vol. 42","author":"Nebel","year":"1995","journal-title":"J. ACM"},{"issue":"1","key":"10.1016\/S0004-3702(00)00070-9_ID068","first-page":"69","article-title":"Translation methods for non-classical logics\u2014An overview","volume":"Vol. 1","author":"Ohlbach","year":"1993","journal-title":"J. Interest Group in Pure and Applied Logic"},{"key":"10.1016\/S0004-3702(00)00070-9_ID069","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","article-title":"HARP: A tableau-based theorem prover","volume":"Vol. 4","author":"Oppacher","year":"1988","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0004-3702(00)00070-9_ID070","series-title":"Proc. 1998 Internat. Workshop on Description Logics","article-title":"DLP system description","author":"Patel-Schneider","year":"1998"},{"key":"10.1016\/S0004-3702(00)00070-9_ID071","series-title":"Proc. 10th ACM Symposium on Theory of Computing (STOC'78), San Diego, CA","first-page":"326","article-title":"A practical decision method for propositional dynamic logic","author":"Pratt","year":"1978"},{"key":"10.1016\/S0004-3702(00)00070-9_ID072","series-title":"Proc. 20th Annual Symposium on the Foundations of Computer Science (FOCS'79)","first-page":"115","article-title":"Models of program logics","author":"Pratt","year":"1979"},{"issue":"1\u20132","key":"10.1016\/S0004-3702(00)00070-9_ID073","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0004-3702(99)00002-8","article-title":"On the complexity of qualitative spatial reasoning: A maximal tractable fragment of the region connection calculus","volume":"Vol. 108","author":"Renz","year":"1999","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0004-3702(00)00070-9_ID074","series-title":"Proc. IJCAI-91, Sydney, Australia","first-page":"466","article-title":"A correspondence theory for terminological logics: Preliminary report","author":"Schild","year":"1991"},{"issue":"4","key":"10.1016\/S0004-3702(00)00070-9_ID075","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1023\/A:1006043519663","article-title":"Decidability by resolution for propositional modal logics","volume":"Vol. 22","author":"Schmidt","year":"1999","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0004-3702(00)00070-9_ID076","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","article-title":"Attributive concept descriptions with complements","volume":"Vol. 48","author":"Schmidt-Schau\u00df","year":"1991","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0004-3702(00)00070-9_ID077","series-title":"Automation of Reasoning (Classical Papers on Computational Logic), Vol. 1 (1957\u20131966)","article-title":"An algorithm for machine search of a natural logical deduction in a propositional calculus","author":"Shanin","year":"1983"},{"key":"10.1016\/S0004-3702(00)00070-9_ID078","series-title":"First Order Logic","author":"Smullyan","year":"1968"},{"issue":"4","key":"10.1016\/S0004-3702(00)00070-9_ID079","doi-asserted-by":"crossref","first-page":"549","DOI":"10.2307\/2271361","article-title":"Uniform Gentzen systems","volume":"Vol. 33","author":"Smullyan","year":"1968","journal-title":"J. Symbolic Logic"},{"issue":"1","key":"10.1016\/S0004-3702(00)00070-9_ID080","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1137\/S0097539790189733","article-title":"Unique binary-search-tree representations and equality testing of sets and sequences","volume":"Vol. 23","author":"Sundar","year":"1994","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0004-3702(00)00070-9_ID081","series-title":"Proc. 16th International Conference on Automated Deduction (CADE'99)","first-page":"52","article-title":"A PSPACE algorithm for graded modal logic","volume":"Vol. 1632","author":"Tobies","year":"1999"},{"issue":"4","key":"10.1016\/S0004-3702(00)00070-9_ID082","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","article-title":"The complexity of propositional proofs","volume":"Vol. 1","author":"Urquhart","year":"1995","journal-title":"Bull. Symbolic Logic"},{"key":"10.1016\/S0004-3702(00)00070-9_ID083","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","article-title":"Automata-theoretic techniques for modal logics of programs","volume":"Vol. 32","author":"Vardi","year":"1986","journal-title":"J. Comput. System Sci."},{"issue":"1","key":"10.1016\/S0004-3702(00)00070-9_ID084","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning about infinite computations","volume":"Vol. 115","author":"Vardi","year":"1994","journal-title":"Inform. and Comput."},{"issue":"3","key":"10.1016\/S0004-3702(00)00070-9_ID085","first-page":"69","article-title":"A knowledge-based configurator that supports sales, engineering, and manufacturing at AT&T network systems","volume":"Vol. 14","author":"Wright","year":"1993","journal-title":"AI Magazine"},{"issue":"2","key":"10.1016\/S0004-3702(00)00070-9_ID086","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/0304-3975(94)90036-1","article-title":"An algorithm for dynamic subset and intersection testing","volume":"Vol. 129","author":"Yellin","year":"1994","journal-title":"Theoret. Comput. Sci."}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370200000709?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370200000709?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T15:30:18Z","timestamp":1578583818000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0004370200000709"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,11]]},"references-count":80,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,11]]}},"alternative-id":["S0004370200000709"],"URL":"https:\/\/doi.org\/10.1016\/s0004-3702(00)00070-9","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[2000,11]]}}}