{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T00:36:37Z","timestamp":1649205397435},"reference-count":26,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.113.6","type":"journal-article","created":{"date-parts":[[2013,3,28]],"date-time":"2013-03-28T13:09:00Z","timestamp":1364476140000},"page":"27-44","source":"Crossref","is-referenced-by-count":1,"title":["Symmetries in Modal Logics"],"prefix":"10.4204","volume":"113","author":[{"given":"Carlos","family":"Areces","sequence":"first","affiliation":[{"name":"FaMAF - Universidad Nacional de C\u00f3rdoba, CONICET"}]},{"given":"Guillaume","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"FaMAF - Universidad Nacional de C\u00f3rdoba"}]},{"given":"Ezequiel","family":"Orbe","sequence":"additional","affiliation":[{"name":"FaMAF - Universidad Nacional de C\u00f3rdoba, CONICET"}]}],"member":"2720","published-online":{"date-parts":[[2013,3,28]]},"reference":[{"issue":"9","key":"Aloul:2002ww","doi-asserted-by":"publisher","first-page":"1117","DOI":"10.1109\/TCAD.2003.816218","article-title":"Solving difficult instances of Boolean satisfiability in the presence of symmetry","volume":"22","author":"Aloul","year":"2003","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"arec:hybr05b","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1016\/S1570-2464(07)80017-6","article-title":"Hybrid Logics","volume-title":"Handbook of Modal Logics","author":"Areces","year":"2006"},{"key":"arec:tree00","first-page":"199","article-title":"Tree-Based Heuristics in Modal Theorem Proving","volume-title":"Proceedings of ECAI'2000","author":"Areces","year":"2000"},{"issue":"4","key":"arec:coin10","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/j.jal.2010.08.010","article-title":"Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)","volume":"8","author":"Areces","year":"2010","journal-title":"Journal of Applied Logic"},{"issue":"1","key":"arec:reso08","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-010-9167-0","article-title":"Resolution with Order and Selection for Hybrid Logics","volume":"46","author":"Areces","year":"2011","journal-title":"Journal of Automated Reasoning"},{"key":"Audemard:2002ti","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-45620-1_19","article-title":"Reasoning by symmetry and function ordering in finite model generation","volume-title":"Proceedings of CADE-18","author":"Audemard","year":"2002"},{"key":"Audemard:2004up","first-page":"257","article-title":"Dealing with Symmetries in Quantified Boolean Formulas","volume-title":"Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04)","author":"Audemard","year":"2004"},{"key":"Benhamou:uv","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1109\/ICTAI.2010.55","article-title":"Enhancing Clause Learning by Symmetry in SAT Solvers","volume-title":"Proceedings of the 22nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI)","author":"Benhamou","year":"2010"},{"key":"Benhamou:1992vx","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/3-540-55602-8_172","article-title":"Theoretical Study of Symmetries in Propositional Calculus and Applications","volume-title":"Proceedings of CADE-11","author":"Benhamou","year":"1992"},{"issue":"1","key":"Benhamou:1994tr","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/BF00881844","article-title":"Tractability Through Symmetries in Propositional Calculus","volume":"12","author":"Benhamou","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"MLBOOK","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn","year":"2001"},{"key":"BBW06","series-title":"Studies in Logic and Practical Reasoning","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-2464(07)80004-8","volume-title":"Handbook of Modal Logic","volume":"3","author":"Blackburn","year":"2006"},{"issue":"3","key":"Brown:1989uw","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-51083-4_51","article-title":"Backtrack searching in the presence of symmetry","volume":"3","author":"Brown","year":"1996","journal-title":"Nordic Journal of Computing"},{"key":"Crawford:1992wz","first-page":"17","article-title":"A Theoretical Analysis of Reasoning By Symmetry in First-Order Logic","volume-title":"Proceedings of AAAI Workshop on Tractable Reasoning","author":"Crawford","year":"1992"},{"key":"Crawford:1996wa","first-page":"148","article-title":"Symmetry-Breaking Predicates for Search Problems","volume-title":"Proceedings of KR 1996","author":"Crawford","year":"1996"},{"key":"Darga:2004us","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1145\/996566.996712","article-title":"Exploiting structure in symmetry detection for CNF","volume-title":"Design Automation Conference, 2004. Proceedings. 41st","author":"Darga","year":"2004"},{"key":"fontaine2011","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-22438-6_18","article-title":"Exploiting Symmetry in SMT Problems","volume-title":"Proceedings of CADE-23","volume":"6803","author":"D\u00e9harbe","year":"2011"},{"key":"Een:2004uh","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","article-title":"An Extensible SAT-solver","volume-title":"Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03)","author":"Een","year":"2003"},{"key":"fraleigh2003first","series-title":"Addison-Wesley world student series","volume-title":"A first course in abstract algebra","author":"Fraleigh","year":"2003"},{"issue":"4","key":"hoffmann2010tab","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jal.2010.08.003","article-title":"Lightweight Hybrid Tableaux","volume":"8","author":"Hoffmann","year":"2010","journal-title":"Journal of Applied Logic"},{"key":"Junttila:2007vx","doi-asserted-by":"crossref","DOI":"10.1137\/1.9781611972870.13","article-title":"Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs","volume-title":"Proceedings of the Workshop on Algorithm Engineering and Experiments, ALENEX 2007","author":"Junttila","year":"2007"},{"issue":"4","key":"KaSmoJoLLI2009","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/s10849-009-9087-8","article-title":"Terminating Tableau Systems for Hybrid Logic with Difference and Converse","volume":"18","author":"Kaminski","year":"2009","journal-title":"Journal of Logic, Language and Information"},{"issue":"3","key":"Krishnamurthy:1985ug","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BF00265682","article-title":"Short Proofs for Tricky Formulas","volume":"22","author":"Krishnamurthy","year":"1985","journal-title":"Acta Informatica"},{"key":"sebastiani","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1613\/jair.1166","article-title":"A New General Method to Generate Random Modal Formulae for Testing Decision Procedures","volume":"18","author":"Patel-Schneider","year":"2003","journal-title":"Journal of Artificial Intelligence Research"},{"key":"Prasad05asurvey","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","article-title":"A survey of recent advances in SAT-based formal verification","volume":"7","author":"Prasad","year":"2005","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"ryan","volume-title":"Efficient Algorithms For Clause-Learning SAT Solvers","author":"Ryan","year":"2004"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2019,7,11]],"date-time":"2019-07-11T13:31:36Z","timestamp":1562851896000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1303.7327v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,28]]},"references-count":26,"URL":"https:\/\/doi.org\/10.4204\/eptcs.113.6","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,28]]}}}