Cláudia Nalon

I'm a full professor at the Department of Computer Science at the University of Brasília. I'm interested in proof methods for combined modal logics, in particular when the resulting language allows for interaction between its components. My PhD was about a resolution-based method for a particular interaction (no learning) between a linear-time temporal logic and multi-modal S5. I have also worked on tableau-based methods for temporal logics of knowledge with either no learning or perfect recall. I am interested in both the theoretical foundations and implementation of reasoning tools for normal modal logics and have worked on proof methods for languages that extend the basic normal modal logic K (allowing symmetry, reflexivity, seriality, transitivity, Euclideaness, and also parametrised multi-modal confluent logics). Very recently, I have worked on a resolution method for Coalition Logics, a non-normal modal logic for reasoning about cooperative agency.

Christopher W. Brown, Daniela Kaufmann, Cláudia Nalon, Alexander Steen, Martin Suda (editors)
PAAR+SC-Square 2024 Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2024.

Joint Proceedings, events co-located with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Nancy, France, July 2, 2024. CEUR Workshop Proceedings 3717, CEUR-WS.org 2024. Open Access. DOI:

Bonacina, M. P., Fontaine, P., Nalon, C. Schon, C., and Desharnais, M. (editors)
The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23741)

Dagstuhl Reports. Volume 13, Issue 11, Pages 130-150. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2024. Open Access. DOI: 10.4230/DagRep.13.11.130.

Pattinson, D. and Nalon, C.
Non-Iterative Modal Resolution.

in the Proceedings of the 12th International Joint Conference on Automated Reasoning, IJCAR 2024, Part II, Nancy, France, July 3–6, 2024. Benzmüller, C., Heule, Marijn J. H., and Schmidt, Renate A. (editors). Lecture Notes in Artificial Intelligence, volume 14740, pages 97-113, 2024. Springer. DOI: 10.1007/978-3-031-63501-4_6. Open Access.

Hustadt, U., Papacchini, F., Nalon, C., and Dixon, C..
Model Construction for Modal Clauses.

in the Proceedings of the 12th International Joint Conference on Automated Reasoning, IJCAR 2024, Part II, Nancy, France, July 3–6, 2024. Benzmüller, C., Heule, Marijn J. H., and Schmidt, Renate A. (editors). Lecture Notes in Artificial Intelligence, volume 14740, pages 3-33, 2024. Springer. DOI: 10.1007/978-3-031-63501-4_1. Open Access.

Pattinson, D, Olivetti, N., and Nalon, C.
Resolution Calculi for Non-normal Modal Logics.

in the Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2023, Prague, Czech Republic. Ramanayake, R. and Urban, J. (editors) Lecture Notes in Artificial Intelligence, volume 14278, pages 322-341, 2023. Springer. DOI: 10.1007/978-3-031-43513-3\_18. Open Access.

Nalon, C., Hustadt, U., Papacchini, F., and Dixon, C.
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic

in the Proceedings of the 29th International Conference on Automated Deduction (CADE-29), 01-04 July, Rome, Italy. Pientka, B. and Tinelli, C. (editors). Lecture Notes in Artificial Intelligence, volume 14132, pages 382-400, 2023. Springer. DOI: 10.1007/978-3-031-38499-8_22. Open Access.

Nalon, C., Hustadt, U., Papacchini, F., and Dixon, C.
Local Reductions for the Modal Cube

in the Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR 2022), held as part of the 8th Federated Logic Conference (FLoC 2022), 8th-11th August, Haifa, Israel. Blanchette, J., Kovacs, L., and Pattinson, D. (editors). Lecture Notes in Computer Science, volume 13385, pages 486-505, 2022. Springer. DOI: 10.1007/978-3-031-10769-6_29. Open Access.

Alkmim, B., Haeusler, E. H, and Nalon, C.
A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals

in the Proceedings of the 35th International Workshop on Description Logics (DL 2022), held as part of the 8th Federated Logic Conference (FLoC 2022), 7th-11th August, Haifa, Israel. Arieli, O., Homola, M., Jung, J. C., and Mugnier, M-L. (editors). CEUR Workshop Proceedings, volume 3263, 2022. Open Access.

Nalon, C. and Pimentel, E. (editors).
Anais do III Workshop Brasileiro de Lógica (WBL)

Open Access. DOI:10.5753/wbl.2022.

Papacchini, F., Nalon, C., Hustadt, U., and Dixon, C.
Local is Best: Efficient Reductions to Modal Logic K

Journal of Automated Reasoning, 2022. Online First: 23/05/2022. DOI: 10.1007/s10817-022-09630-6. Open Access.

Silva, G. G. F. da, Haeusler, E. H., and Nalon, C.
Description of Command and Control Networks in Coq

in Anais do Workshop-Escola de Informática Teórica 2021 (WEIT 2021), pages 60-67, 2021. Santos, H., Ferreira, A. P. L., Heiser, R. H. S. (editors), SBC, Brazil. DOI: 10.5753/weit.2021.18923. Open Access.

Papacchini, F., Nalon, C., Hustadt, U., and Dixon, C.
Efficient Local Reductions to Basic Modal Logic

in the Proceedings of the 28th International Conference on Automated Deduction (CADE-28). Platzer, A. and Sutcliffe, G. (editors). Lecture Notes in Artificial Intelligence 12699, pages 76-92, 2021. Springer. DOI: 10.1007/978-3-030-79876-5_5. Open Access.

Lopes, B., Nalon, C., and Hauesler, E. H.
Reasoning about Petri nets: a calculus based on Resolution and Dynamic Logic

ACM Transactions on Computational Logic. Volume 22 Issue 2, May 2021, Article No. 9, 9:1-9:22. ACM, 2021.

Nalon, C. and Reis, G. (editors)
Proceedings of LSFA 2020, the 15th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2020)

Electronic Notes in Theoretical Computer Science. Volume 351. Elsevier, 2020. DOI:10.1016/j.entcs.2020.08.001. Open Access.

Beyersdorff, O., Egly, U., Mahajan, M., Nalon, C. (editors)
SAT and Interactions (Dagstuhl Seminar 20061)

Dagstuhl Reports. Volume 10(2). Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2020. DOI:10.4230/DagRep.10.2.1. Open Access.

Nalon, C., Hustadt, U., and Dixon, C.
KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments

Journal of Automated Reasoning. Volume 64(3), pages 461-484. Springer, 2020. DOI:10.1007/s10817-018-09503-x. Open Access. Online first: 17th December 2018.

Nalon, C., Dixon, C., and Hustadt, U.
Modal Resolution: Proofs, Layers, and Refinements

ACM Transactions on Computational Logic. Volume 20 Issue 4, September 2019, Article No. 23, 23:1-23:38. ACM, 2019. DOI:10.1145/3331448. Open Access.

Hustadt, U., Nalon, C., and Dixon, C.
Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics

in the Proceedings of 6th Workshop on Practical Aspects of Automated Reasoning, PAAR 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018. CEUR Workshop Proceedings, 2162, pages 34-48, 2018.

Nalon, C. and Pattinson, D.
A Resolution-Based Calculus for Preferential Logics

in the Proceedings of the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, held as part of the Federated Logic Conference, FloC 2018, Galmiche, D., Schulz, S. and Sebastiani, R. (Editors), Oxford, UK, July 14-17, 2018. Lecture Notes in Computer Science, 10900, pages 498-515, 2018. Springer DOI:10.1007/978-3-319-94205-6_33.

Nalon, C. and Angelos, D.
On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving

Accepted for publication in the Proceedings of Women in Logic, WiL 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018.

Nalon, C., Hustadt, U., and Dixon, C.
Separated Normal Form Transformation Revisited

in Proceedings of the 25th Automated Reasoning Workshop, Bridging the Gap between Theory and Practice (ARW 2018), Jamnik, M., Koutsoukou-Argyraki, A., Ayers, E., and Mangla, C. (Editors), pages 6-7, 12th and 13th of April, 2018, Cambridge, UK.

Papacchini, F., Nalon, C., Hustadt, U., and Dixon, C.
Extending the KSP Prover to More Expressive Modal Logics

in Proceedings of the 25th Automated Reasoning Workshop, Bridging the Gap between Theory and Practice (ARW 2018), Jamnik, M., Koutsoukou-Argyraki, A., Ayers, E., and Mangla, C. (Editors), pages 21-22, 12th and 13th of April, 2018, Cambridge, UK.

Schmidt,R. A., and Nalon, C. (editors)
Automated Reasoning with Analytic Tableaux and Related Methods, the 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28,2017, Proceedings

Volume 10501 of Lecture Notes in Artificial Intelligence. Springer International Publishing, 2017. ISBN 978-3-319-66902-1, DOI 10.1007/978-3-319-66902-1

Nalon, C., Hustadt, U., and Dixon, C.
KSP: a resolution-based prover for multimodal K, Abridged Report

in Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017. Carles Sierra (editor). Pages 4919-4923. DOI: 10.24963/ijcai.2017/694.

Marcos, J., and Nalon, C.
Classical Resolution for Many-Valued Logics

in Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015). Benevides, M. and Thiemann, R. (editors). Electronic Notes in Theoretical Computer Science, 323, pages 253-270. Elsevier, 2016. DOI: 10.1016/j.entcs.2016.09.001. Open Access.

Nalon, C., Hustadt, U., and Dixon, C.
KSP: a resolution-based prover for multimodal K

in Proceedings of Automated Reasoning: 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016. Olivetti, N. and Tiwari, A. (editors). Lecture Notes in Computer Science, 9706, pages 406--415. Springer, 2016. DOI: 10.1007/978-3-319-40229-1_28.

Nalon, C., Hustadt, U., and Dixon, C.
A Modal-Layered Resolution Calculus for K

in Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21-24, 2015. de Nivelle, H. (editor). Lecture Notes in Computer Science, 9323, pages 185--200. Springer, 2015. DOI: 10.1007/978-3-319-24312-2_13

Hustadt, U., Gainer, P., Dixon, C., Nalon, C., and Zhang, L.
Ordered Resolution for Coalition Logic

in Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21-24, 2015. de Nivelle, H. (editor). Lecture Notes in Computer Science, 9323, pages 169--184. Springer, 2015. DOI: 10.1007/978-3-319-24312-2_12

Nalon, C., Lopes, B., Dowek, G., and Haeusler, E. H.
A Calculus for Automatic Verification of Petri Nets Based on Resolution and Dynamic Logics

Electronic Notes in Theoretical Computer Science 312 (2015) 125–141. Open Access. DOI:10.1016/j.entcs.2015.04.008

Hustadt, U., Gainer, P., Dixon, C., Nalon, C., and Zhang, L.
CLProver++: An Ordered Resolution Prover for Coalition Logic

in the proceedings of the Automated Reasoning Workshop 2015 - Bridging the Gap between Theory and Practice - ARW 2015. Sorge, V. (Ed.), Birmingham, UK, pages 27-28, 9-10 April, 2015.

Dixon, C., Nalon, C., and Ramanujam, R.
Knowledge and Time

in Handbook of Epistemic Logic. van Ditmarsch, H., Halpern, J. Y., van der Hoek, W. and Kooi, B. (Editors). Pages 205-259. College Publications. London, UK. 2015. ISBN 978-1-84890-158-2.

Nalon, C., Marcos, J., and Dixon, C.
Clausal Resolution for Modal Logics of Confluence

7th International Joint Conference on Automated Reasoning, held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings. Demri, S., Kapur, D., and Weidenbach, C. (Eds.). Lecture Notes in Artificial Intelligence, 8562, pp. 322-336. Springer, 2014. DOI: 10.1007/978-3-319-08587-6_24

Nalon, C. and Kutz, O.
Towards Resolution-based Reasoning for Connected Logics.

Proceedings of the 8th Workshop on Logical and Semantical Frameworks, with Applications (LSFA). Fernández, M. and Finger, M. (Editors). São Paulo, Brazil, 2-3 September, 2013. Electronic Notes in Theoretical Computer Science, volume 305, pages 85-102, 2014. Open Access. DOI: 10.1016/j.entcs.2014.06.007

Nalon, C., Zhang, L., Dixon, C., and Hustadt, U.
A Resolution Prover for Coalition Logic.

Proceedings of the 2nd International Workshop on Strategic Reasoning. Mogavero, F., Murano, A., and Vardi, M. Y. (Editors). Grenoble, France, April 5-6, 2014. Electronic Proceedings in Theoretical Computer Science, volume 146, pages 65-73. Open Publishing Association, 2014. DOI:10.4204/EPTCS.146.9

Nalon, C., Zhang, L., Dixon, C., and Hustadt, U.
A resolution-based calculus for Coalition Logic.

Journal of Logic and Computation, v. 24 (4), pages 883-917. Oxford University Press, 2014. Open Access. DOI:10.1093/logcom/ext074.

Nalon, C., Marcos, J., and Dixon, C.
Clausal Resolution for Modal Logics of Confluence -- Extended Version

This is an extended version, including correctness proofs, of the paper ``Clausal Resolution for Modal Logics of Confluence'' published in the proceedings of IJCAR 2014.

Vieira, T. C. and Nalon, C.
Verificação Epistêmico-Temporal via Tradução.

Anais do II WEIT 2013, de Aguiar, M. S., Barbosa, R. de M., Cavalheiro, S. A. da C., Dimuro, G. P., Duarte, L. M., Foss, L., Gonçalves, E. M. N., e Ribeiro, L. (Orgs.), Ed. da Universidade Federal do Rio Grande - FURG, Rio Grande, 2013.

Nalon, C. and Kutz, O.
Towards Resolution-based Reasoning for Connected Logics.

in the pre-proceedings of LSFA 2013, 8th Workshop on Logical and Semantical Frameworks, with Applications. Fernández, M. and Finger, M. (editors) pages 36--51, São Paulo, Brazil, 2013.

Nalon, C., Zhang, L., Dixon, C., and Hustadt, U.
A resolution-based calculus for Coalition Logic (Extended Version).

Technical Report ULCS-13-004, University of Liverpool, UK, 2013.

Nalon, C. and Dixon, C.
Clausal Resolution for Normal Modal Logics.

Journal of Algorithms, Volume 62, Issues 3-4, July-October 2007, Pages 117-134.

Nalon, C. and Dixon, C.
Normal Modal Resolution: Preliminary Results

in the Proceedings of Logical and Semantic Frameworks, with Applications (LSFA'06), Natal, RN, Brazil, 17th, September, 2006, pp. 38-46.

Nalon, C. and Dixon, C.
Anti-Prenexing and Prenexing for Modal Logics

in the Proceedings of the 10th European Conference on Logics in Artificial Intelligence -- JELIA'06, Liverpool, UK, 13-15, September, 2006. Lecture Notes in Computer Science, Volume 4160/2006, pp. 333-345. ISSN 0302-9743.

Nalon, C. and Dixon, C.
Anti-Prenexing and Prenexing for Modal Logics (Extended Version)

Technical Report ULCS-06-003, University of Liverpool, UK, 2006.

Nalon, C.
Normal Forms for Modal Logics

Ninth Workshop on Automated Reasoning - ARW 2006 - Bristol, UK, 3-4 April, 2006.

Nalon, C., Dixon, C., and Fisher, M.
Resolution for Synchrony and No Learning

in Advances in Modal Logic, volume 5. Schmidt, R., Pratt-Hartmann, I., Reynolds, M., and Wansing, H. (Editors). King's College Publications, UK, 2005, pp. 231--248 (ISBN 1904987222).

Dixon, C., Nalon, C., and Fisher, M.
Tableaux for Logics of Time and Knowledge with Interactions Relating to Synchrony

Journal of Applied Non-Classical Logics, Vol. 14 -- No. 4/2004, pp. 397--445. Lavoisier. Paris, 2004.

Nalon, C., Dixon, C. and Fisher, M.
Resolution for Synchrony and No Learning

in the Proceedings of AiML'04, 9-11 September, 2004, Manchester.

Dixon, C., Nalon, C., and Fisher, M.
Tableaux for Temporal Logics of Knowledge: Synchronous Systems of Perfect Recall or No Learning

in the Proceedings of TIME-ICTL 2003, 8-10 July, 2003, Cairns, Queensland, Australia. IEEE.

Nalon, C., Dixon, C., and Fisher, M.
Resolution for Temporal Logics of Knowledge with Interactions

Ninth Workshop on Automated Reasoning - ARW 2002 - London, UK, 3-4 April, 2002.

Nalon, C., Dixon, C., and Fisher, M.
Resolution for Synchrony and No Learning: Preliminary Report

in the Proceedings of the 8th International Workshop on Logic Language, Information and Computation WoLLIC'2001, de Queiroz, R., and Ayala-Rincon, M. (eds.), 2001.
Abstract available in the WoLLIC'2001 Conference Report. In Logic Journal of the Interest Group in Pure and Applied Logics 9(5):739-754, Oxford University Press, September 2001.

Nalon, C.
Theorem-Proving for Synchronous Systems with no Learning

Eighth Workshop on Automated Reasoning - ARW 2001 - York, UK, 22-23, March, 2001.

Nalon, C.
Theorem-Proving for Temporal Logics of Knowledge and Belief

Seventh Workshop on Automated Reasoning - ARW'2000 - London, UK, July, 2000.

Nalon, C. and Wainer, J.
Strong Conditional Logic

in the Proceedings of the 14th Brazilian Symposium on Artificial Intelligence, SBIA '98, Porto Alegre, Brazil, November 4-6, 1998, de Oliveira, F. M. (Ed.), Advances in Artificial Intelligence, Lecture Notes in Computer Science 1515 Springer 1998,  pages 209-218. DOI: 10.1007/10692710_22.

Nalon, C. and Wainer, J.
Construção de Modelos Condicionais Com Boas Propriedades

I Artificial Intelligence National Meeting (ENIA), Brazilian Computer Society, Brasília, Brazil, August, 1997.

Nalon, C. and Wainer, J.
Constructing Models with Good Properties: Preliminary Results

in the Proceedings of the XVI International Conference of the Chilean Computer Science Society. Zelkowitz, M. V. and Straub, P. (eds.), Valdivia, Nov. 1996, Sociedad Chilena de Ciencia de Computacion (SCCC), 1996.

I am a member of the editorial board of the IfCoLog Journal of Logics and their Applications, since 2015.

I am/was a member of the steering committee of the following conferences:

I am/was a member of the executive committee of the Brazilian Logic Society (2017-2019, 2019-2021).

I am/was invited speaker of the following conferences:

I am/was a panel member of the CADE ATP System Competition; see in 2022, CASC-29 in 2023, and in 2024.

I am/was a member of the program committees of the following conferences:

KR 2016 - The 15th International Conference on Principles of Knowledge Representation and Reasoning

Cape Town, South Africa, April 25-29, 2016.

TABLEAUX 2015 - 24th Conference on Automated Reasoning with Analytic Tableaux and Related Methods

University of Wrocław, Poland, September 20-24, 2015.

CTD - XXVI Concurso de Teses e Dissertações, SBC

Maceió, Brazil, July, 2013.

LSFA 2011 - The 6th Workshop on Logical and Semantic Frameworks, with Applications

Belo Horizonte, Brazil, August 27, 2011.

LSFA 2010 - The 5th Workshop on Logical and Semantic Frameworks, with Applications

Natal, Brazil, August 31, 2010.

October, 2023

Seminar, Modal Sessions I, Modal Sessions II, Modal Sessions III

August, 2019

Machine-Oriented Reasoning. (Invited Tutorial at CADE-27)

August, 2015

Machine-Oriented Reasoning (syllabus) [Portuguese]

June, 2008

CIC - UnB - MAS - Part 1 [Portuguese]

CIC - UnB - MAS - Part 2 [Portuguese]

July, 2006

May, 2006

March, 2006

December, 2005

October, 2004

I have implemented the following:

The following are provers implemented by students I have supervised:

Aperfeiçoamento da escrita técnica em Computação. [This page is in Portuguese]

The project aim was to help improving the writing skills of students taking modules offered by the Department of Computer Science. Instead of providing a service for correcting texts, we pointed out the mistakes occuring in the text and mentioned the corresponding grammar rules, so that the students became aware of where they were doing wrong, why they were doing wrong, and how they could fix the text by themselves. I was the coordinator for this project during 2010, 2011, and the first semester of 2013, when it was discontinuated.

Meninas.comp. [This page is in Portuguese]

The project aim is to bring awareness of the gender gap in STEM, particularly within Computer Science. We had several activities involving programming, lectures, talks, directed to girls at school age. I was the coordinator of this project during 2010 and 2011, but I am no longer involved.