About

Photo - CN

Cláudia Nalon

I'm an associate 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.

Publications

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

Journal of Automated Reasoning. Accepted for publication (2018).

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. and 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.

R. A. Schmidt and C. Nalon (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.

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.

Activities

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

I am a member of the steering committee of TABLEAUX (ex-officio, representative of TABLEAUX 2017, 2016-2018).

I am member of the executive committee of the Brazilian Logic Society (2017-2019).

I am/was invited speaker of the following conferences:

WiL - Women in Logic Workshop

Reykjavik, Iceland, June 18-19, 2017.

Afilliated with the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 20–23 June 2017, Reykjavik, Iceland.

XVIII Brazilian Logic Conference

Pirenópolis, Brazil, May 8-12, 2017.

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

EBL 2019 - The 19th Brazilian Logic Conference

João Pessoa, Paraíba, Brazil, 6-10 May, 2019

PAAR-2018 - The 6th Workshop on Practical Aspects of Automated Reasoning

Oxford, UK, July 19, 2018.

Held as part of the Federated Logic Conference 2018 (FLOC 2018), Oxford, UK, July 6-19, 2018.

IJCAR 2018 - The 9th International Joint Conference on Automated Reasoning

Oxford, UK, July 14-17, 2018.

Held as part of the Federated Logic Conference 2018 (FLOC 2018), Oxford, UK, July 6-19, 2018.

M4M9 - Methods for Modalities

Kanpur, India, January 08-10, 2017.

ETMF - Escola de Informática Teórica e Métodos Formais

Natal, Brazil, November 22-23, 2016.

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

Porto Alegre, Brazil, July, 2016.

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

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

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

SAT and Interactions, part of the Dagstuhl Seminars and Perspectives Workshops

CADE-27 - The 27th International Conference on Automated Deduction

TABLEAUX 2017 - The 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods

FroCoS 2017 - The 11th International Symposium on Frontiers of Combining Systems

ITP 2017 - The 8th International Conference on Interactive Theorem-Proving

LSFA 2014 - The 9th Workshop on Logical and Semantic Frameworks, with Applications

WOLLIC 2010 - The 17th Workshop on Logic, Language, Information and Computation

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

LSFA 2009 - The 4th Workshop on Logical and Semantic Frameworks, with Applications

Slides/Seminars

August, 2015

Machine-Oriented Reasoning (syllabus) [Portuguese]

June, 2008

CIC - UnB - MAS - Part 1 [Portuguese]

CIC - UnB - MAS - Part 2 [Portuguese]

July, 2006

CIC - UnB [Portuguese]

May, 2006

IME - USP [Portuguese]

March, 2006

LOCO seminar -LIVERPOOL (pdf) (ps)

December, 2005

Informal (, mas formal!) MAT - UnB [Portuguese]

October, 2004

Informal (, mas formal!) MAT - UnB [Portuguese]

Software

I have implemented the following:

ltl2snf

ltl2snf is an implementation, written in C, for the translator of formulae in the language of propositional temporal into a set of clauses in Separated Normal Form (in the language of TRP++). The source, together with instructions on how to install and run the prover, can be downloaded by clicking here.

ltl2snf by Cláudia Nalon is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License. You are free to use, share and adapt the code under the following restrictions: (BY) you must give appropriate credit for the material you are using/adapting; (SA) your contribution must be shared under the same licence; and (NC) you may not use the material for commercial purposes. Also, you may not apply legal terms or technological measures that legally restrict others from doing anything the license permits. Please follow the link and read the licence for full terms and conditions.

KSP

KSP is an implementation, written in C, for the resolution calculus described in the paper "A Modal-Layered Resolution Calculus for K" (Nalon, C., Hustadt, U., and Dixon, C., TABLEAUX proceedings, 2015). The theorem-prover is primarily based on the set of support strategy, which can be combined with other strategies and different choices for the underlying normal form. The source, together with instructions on how to install and run the prover, can be downloaded by clicking here (IJCAR 2016) or here (JAR 2017).

We have evaluated KSP on both traditional sets of formulae (LWB, MQBF) and on randomly generated sets of formulae (3CNF). The LWB generator can be downloaded by clicking here. This bash script generates the files listed in "List_of_LWB_benchmark_files.txt" distributed with the LWB generator (except for the k_ph files; please see the README in the generator package). You can also download this perl script which takes the intohylo files as input and generates the files with the KSP syntax.

KSP by Cláudia Nalon is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License. You are free to use, share and adapt the code under the following restrictions: (BY) you must give appropriate credit for the material you are using/adapting; (SA) your contribution must be shared under the same licence; and (NC) you may not use the material for commercial purposes. Also, you may not apply legal terms or technological measures that legally restrict others from doing anything the license permits. Please follow the link and read the licence for full terms and conditions.

CLProver: A Theorem-Prover for Coalition Logic

This is a prototype implementation of a theorem-prover based on the method described in the paper "A resolution-based calculus for Coalition Logic" (Nalon, C., Zhang, L., Dixon, C., and Hustadt, U., Journal of Logic and Computation, 2014). The binary (SWI Prolog compiled for linux, x86_64, stand alone version, with global stack of 5GB) together with instructions for running the prover and few examples can be downloaded by clicking here. The prover deals with the satisfiability problem for coalition problems, as defined in the above mentioned paper. The prover is available for use "as it is". I intend to provide the sources in the near future as open source. If you have any questions regarding the prover, feel free to contact me.

Synchronous Systems with No Learning

A prototype version of the prover for synchronous systems with no learning can be downloaded by clicking here. You'll need Otter, SWI-Prolog, and Emacs to run the prover. Instructions can be found here. Last updated: 08/06/2004.

The following are provers implemented by students I have supervised:

L3 Prover Based on the Bivalent Translation and MiniSat

The prover for the Lukasiewicz three-valued logic is based on the bivalent translation given on the paper "Classical Resolution for Many-Valued Logics" (J. Marcos and C. Nalon, ENTCS, 2016). After translation, MiniSat is used to check the satisfiability of the resulting set of clauses. The prover was compared to Multseq and the results are also available in the package. The programs were implemented by Matheus Bastos de Castro as part of his final year project (Prova de Teoremas em Lógica Três-Valorada, 2017), which I have supervised. The sources and results can be downloaded by cliking here.

Simplification Procedures for KSP

Refactoring of pure literal elimination procedures for KSP. The new procedures and data structures were implemented by André Belle Menezes as part of his final year project (Métodos Polinomiais para Simplificação de Fórmulas Modais, 2016), which I have supervised. The source can be downloaded by cliking here.

Theorem-Prover for Multimodal Normal Logics

An implementation of a theorem-prover based on the method described in the paper "Resolution for Normal Modal Logics" (C. Nalon and C. Dixon, Journal of Algorithms, 2007). The prover deals with the satisfiability problem for the multimodal versions of K and systems which include the axioms T, B, D, 4, and 5. The prover was implemented by George Bezerra Silva as part of his final year project (Implementação de um Provador de Teoremas por Resolução para Lógicas Modais Normais, 2013) which I have supervised. Contact me if you have questions about this prover.

Outreach and Other Projects

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.

Contact

Computer Science Department
University of Brasília
Campus Universitário - Asa Norte
Caixa Postal 4466
Brasília - DF - Brazil
CEP: 70.910-090
E-mail: nalon@unb.br
Phone:  +55 61 3107 6390
Fax:       +55 61 3273 3589

This page is maintened by Cláudia Nalon. Last Updated: