@article(Aloul:2002ww,
 author       = "F. Aloul and A. Ramani and I. Markov and K. Sakallah",
 year         = "2003",
 title        = "Solving difficult instances of Boolean satisfiability in the presence of symmetry",
 journal      = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
 volume       = "22",
 number       = "9",
 pages        = "1117--1137",
 doi          = "10.1109/TCAD.2003.816218",
)
@incollection(arec:hybr05b,
 author       = "C. Areces and B. ten Cate",
 year         = "2006",
 title        = "Hybrid Logics",
 editor       = "P. Blackburn and F. Wolter and J. van Benthem",
 booktitle    = "Handbook of Modal Logics",
 publisher    = "Elsevier",
 pages        = "821--868",
 doi          = "10.1016/S1570-2464(07)80017-6",
)
@inproceedings(arec:tree00,
 author       = "C. Areces and R. Gennari and J. Heguiabehere and M. de Rijke",
 year         = "2000",
 title        = "Tree-Based Heuristics in Modal Theorem Proving",
 booktitle    = "Proceedings of ECAI'2000",
 address      = "Berlin, Germany",
 pages        = "199--203",
)
@article(arec:coin10,
 author       = "C. Areces and D. Gor\'{\i }n",
 year         = "2010",
 title        = "Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)",
 journal      = "Journal of Applied Logic",
 volume       = "8",
 number       = "4",
 pages        = "305--318",
 doi          = "10.1016/j.jal.2010.08.010",
)
@article(arec:reso08,
 author       = "C. Areces and D. Gor\'{\i }n",
 year         = "2011",
 title        = "Resolution with Order and Selection for Hybrid Logics",
 journal      = "Journal of Automated Reasoning",
 volume       = "46",
 number       = "1",
 pages        = "1--42",
 doi          = "10.1007/s10817-010-9167-0",
)
@inproceedings(Audemard:2002ti,
 author       = "G. Audemard",
 year         = "2002",
 title        = "Reasoning by symmetry and function ordering in finite model generation",
 booktitle    = "Proceedings of CADE-18",
 pages        = "226--240",
 doi          = "10.1007/3-540-45620-1\_19",
)
@inproceedings(Audemard:2004up,
 author       = "G. Audemard and B. Mazure and L. Sais",
 year         = "2004",
 title        = "Dealing with Symmetries in Quantified Boolean Formulas",
 booktitle    = "Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04)",
 pages        = "257--262",
)
@inproceedings(Benhamou:uv,
 author       = "B. Benhamou and T. Nabhani and R. Ostrowski and M. Saidi",
 year         = "2010",
 title        = "Enhancing Clause Learning by Symmetry in {SAT} Solvers",
 booktitle    = "Proceedings of the 22nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI)",
 pages        = "329--335",
 doi          = "10.1109/ICTAI.2010.55",
)
@inproceedings(Benhamou:1992vx,
 author       = "B. Benhamou and L. Sais",
 year         = "1992",
 title        = "Theoretical Study of Symmetries in Propositional Calculus and Applications",
 booktitle    = "Proceedings of CADE-11",
 pages        = "281--294",
 doi          = "10.1007/3-540-55602-8\_172",
)
@article(Benhamou:1994tr,
 author       = "B. Benhamou and L. Sais",
 year         = "1994",
 title        = "Tractability Through Symmetries in Propositional Calculus",
 journal      = "Journal of Automated Reasoning",
 volume       = "12",
 number       = "1",
 pages        = "89--102",
 doi          = "10.1007/BF00881844",
)
@book(MLBOOK,
 author       = "P. Blackburn and M. {de Rijke} and Y. Venema",
 year         = "2001",
 title        = "Modal Logic",
 publisher    = "Cambridge University Press",
)
@book(BBW06,
 author       = "P. Blackburn and J. {van Benthem} and F. Wolter",
 year         = "2006",
 title        = "Handbook of Modal Logic",
 series       = "Studies in Logic and Practical Reasoning",
 volume       = "3",
 publisher    = "Elsevier Science Inc.",
 address      = "New York, NY, USA",
 doi          = "10.1016/S1570-2464(07)80004-8",
)
@article(Brown:1989uw,
 author       = "C. Brown and L. Finkelstein and P. Purdom, Jr.",
 year         = "1996",
 title        = "Backtrack searching in the presence of symmetry",
 journal      = "Nordic Journal of Computing",
 volume       = "3",
 number       = "3",
 pages        = "203--219",
 doi          = "10.1007/3-540-51083-4\_51",
)
@inproceedings(Crawford:1992wz,
 author       = "J. Crawford",
 year         = "1992",
 title        = "A Theoretical Analysis of Reasoning By Symmetry in First-Order Logic",
 booktitle    = "Proceedings of AAAI Workshop on Tractable Reasoning",
 address      = "San Jose, CA",
 pages        = "17--22",
)
@inproceedings(Crawford:1996wa,
 author       = "J. Crawford and M. Ginsberg and E. Luks and A. Roy",
 year         = "1996",
 title        = "Symmetry-Breaking Predicates for Search Problems",
 booktitle    = "Proceedings of KR 1996",
 pages        = "148--159",
)
@inproceedings(Darga:2004us,
 author       = "P. Darga and M. Liffiton and K. Sakallah and I. Markov",
 year         = "2004",
 title        = "{Exploiting structure in symmetry detection for CNF}",
 booktitle    = "Design Automation Conference, 2004. Proceedings. 41st",
 pages        = "530--534",
 doi          = "10.1145/996566.996712",
)
@incollection(fontaine2011,
 author       = "D. D\'eharbe and P. Fontaine and S. Merz and B. Woltzenlogel Paleo",
 year         = "2011",
 title        = "Exploiting Symmetry in SMT Problems",
 booktitle    = "Proceedings of CADE-23",
 series       = "Lecture Notes in Computer Science",
 volume       = "6803",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "222--236",
 doi          = "10.1007/978-3-642-22438-6\_18",
)
@inproceedings(Een:2004uh,
 author       = "N. Een and N. S{\"o}rensson",
 year         = "2003",
 title        = "An Extensible SAT-solver",
 booktitle    = "Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03)",
 pages        = "502--518",
 doi          = "10.1007/978-3-540-24605-3\_37",
)
@book(fraleigh2003first,
 author       = "J.B. Fraleigh and V.J. Katz",
 year         = "2003",
 title        = "A first course in abstract algebra",
 series       = "Addison-Wesley world student series",
 publisher    = "Addison-Wesley",
)
@article(hoffmann2010tab,
 author       = "G. Hoffmann",
 year         = "2010",
 title        = "Lightweight Hybrid Tableaux",
 journal      = "Journal of Applied Logic",
 volume       = "8",
 number       = "4",
 pages        = "397--408",
 doi          = "10.1016/j.jal.2010.08.003",
)
@inproceedings(Junttila:2007vx,
 author       = "T. Junttila and P. Kaski",
 year         = "2007",
 title        = "Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs",
 booktitle    = "Proceedings of the Workshop on Algorithm Engineering and Experiments, ALENEX 2007",
 publisher    = "SIAM",
)
@article(KaSmoJoLLI2009,
 author       = "M. Kaminski and G. Smolka",
 year         = "2009",
 title        = "Terminating Tableau Systems for Hybrid Logic with Difference and Converse",
 journal      = "Journal of Logic, Language and Information",
 volume       = "18",
 number       = "4",
 pages        = "437--464",
 doi          = "10.1007/s10849-009-9087-8",
)
@article(Krishnamurthy:1985ug,
 author       = "B. Krishnamurthy",
 year         = "1985",
 title        = "Short Proofs for Tricky Formulas",
 journal      = "Acta Informatica",
 volume       = "22",
 number       = "3",
 pages        = "253--275",
 doi          = "10.1007/BF00265682",
)
@techreport(McKay:1990vf,
 author       = "B. McKay",
 year         = "1990",
 title        = "Nauty User's Guide",
 type         = "Technical Report",
 institution  = "Australian National University, Computer Science Department",
)
@techreport(orbe2012,
 author       = "E. Orbe and C. Areces and G. Infante-L\'opez",
 year         = "2012",
 title        = "A Note about Modal Symmetries",
 type         = "Technical Report",
 institution  = "FaMAF, UNC",
 url          = "http://www.famaf.unc.edu.ar/publicaciones/documents/serie_a/AInf6.pdf",
)
@article(sebastiani,
 author       = "P. Patel-Schneider and R. Sebastiani",
 year         = "2003",
 title        = "A New General Method to Generate Random Modal Formulae for Testing Decision Procedures",
 journal      = "Journal of Artificial Intelligence Research",
 volume       = "18",
 pages        = "351--389",
)
@article(Prasad05asurvey,
 author       = "M. Prasad and A. Biere and A. Gupta",
 year         = "2005",
 title        = "A survey of recent advances in {SAT}-based formal verification",
 journal      = "International Journal on Software Tools for Technology Transfer",
 volume       = "7",
 pages        = "156--173",
 doi          = "10.1007/s10009-004-0183-4",
)
@mastersthesis(ryan,
 author       = "L. Ryan",
 year         = "2004",
 title        = "Efficient Algorithms For Clause-Learning {SAT} Solvers",
 school       = "Simon Fraser University",
)