My professional page is no longer hosted by the University of Brasilia. Welcome to my new website!

About

Photo - CN

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.

Publications

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

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.

Activities

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:

The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - TABLEAUX (ex-officio, representative of TABLEAUX 2017, 2016-2019; elected, 2020-2023).

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:

The 17th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2022)

Belo Horizonte, Minas Gerais, Brazil, August 23rd and 24thm 2022.

Logic Mentoring Workshop @CSL, Panel

Göttingen, Germany (virtual), February 14th 2022. Co-located with Computer Science Logic CSL 2022.

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, Goiás, Brazil, May 8-12, 2017.

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

CICM 2024 - The 17th Conference on Intelligent Computer Mathematics

Montréal, Québec, Canada, August 5-9, 2024.

WBL 2023 - IV Workshop Brasileiro de Lógica (Co-Chair)

João Pessoa, PB, Brazil, August 06-11, 2023. Affiliated to the XLIII CSBC (Congresso da Sociedade Brasileira de Computação).

WiL 2023 - Women in Logic

Rome, Italy, July 01, 2023.

WBL 2022 - III Workshop Brasileiro de Lógica (Co-Chair)

Niterói, RJ, Brazil, August 3, 2022. Affiliated to the XLII CSBC (Congresso da Sociedade Brasileira de Computação).

IJCAR 2022 - The 11th International Joint Conference on Automated Reasoning

Haifa, Israel, August 8-10, 2022 (as part of FLoC).

ITP 2022 - The 13th International Conference on Interactive Theorem Proving

Haifa, Israel, August 7-10, 2022 (as part of FLoC).

WBL 2021 - II Workshop Brasileiro de Lógica

Florianópolis, Santa Catarina, Brazil, July 18-22, 2021. Affiliated to the XLI CSBC (Congresso da Sociedade Brasileira de Computação).

CADE-28 - The 28th Conference on Automated Deduction

Pittsburgh, USA, July 11-16, 2021.

LSFA 2020 - The 15th Workshop on Logical and Semantic Frameworks, with Applications (Co-Chair)

Salvador, Bahia, Brazil, August 27-28, 2020.

The 13th Conference on Advances in Modal Logic (AiML 2020)

Helsinki, Finland, August 17-21, 2020.

PAAR-2020 - The 7th Workshop on Practical Aspects of Automated Reasoning

Paris, France, dates to be announced, 2020.

Held as part of The 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June 29-July 05, 2020.

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:

WBL 2022 - III Workshop Brasileiro de Lógica, part of the CSBC 2022 - XLII Congresso da Sociedade Brasileira de Computação

Integrated Deduction, part of the Dagstuhl Seminars and Perspectives Workshops, 2021

WBL 2021 - II Workshop Brasileiro de Lógica, part of the CSBC 2021 - XLI Congresso da Sociedade Brasileira de Computação

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

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

LSFA 2019 - The 14th Workshop on Logical and Semantic Frameworks, with Applications

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

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

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 logic 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 preprocessor, can be downloaded by cliking the desired version:

ltl2snf+ls4 is a small shell script that uses ltl2snf to transform a PLTL formula to SNF and then uses the PLTL prover LS4 to solve it. The source code for LS4 can be found at https://github.com/quickbeam123/ls4.

ltl2snf by Cláudia Nalon and ltl2snf+ls4 by Ullrich Hustadt are both 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 cliking the desired version:

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. The benchmarks used in the evaluation given in the IJCAR 2022 submission can be found here (KSP syntax) and here (intohylo syntax).

For the (submitted) CADE-29 paper, we use the same benchmarks of IJCAR 2022 for the approaches that use the implemented global calculus and internalised reductions implemented in KSP. The input files generated with the definitional reduction and axiomatic reduction for all provers can be found here: input files for CEGARBOX; and in the following external links: input files for Spartacus, and input files for KSP.

For the (submitted) TABLEAUX 2023 paper, we use the same benchmarks of IJCAR 2022 and also the same configuration files. The option -logsimp should be added to the command line to enable logic specific simplification. The configuration files for the logics can be also found together with the configuration files for the IJCAR 2022 submission (that is, in the folder ksp/conf.files/ijcar-2022/).

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:

Preprocessamento de cláusulas para raciocínio local e global no KSP

This is a partial implementation of input processing and preprocessing of clauses in KSP. It was developed by João Victor C. de Melo as part of his final year project. It can be downloaded by clicking here.

Formalização de Resultados Teóricos em Assistente de Provas

This is a formalisation of the syntax, semantics, and negation normal form for the monomodal logic K, developed in Coq by Maria Julia Dias Lima as part of her research induction project (PIBIC 2020-2021, pibic 2021-2022). It can be downloaded by clicking here AND here.

KSP+MiniSat

This is a modification of the KSP prover which uses MiniSat to guide the application of the modal inference rules. The prover was implemented by Daniella Angelos as part of her Master's dissertation (Combining Clause Learning and Resolution for Multimodal Reasoning, 2019), which I have supervised. The sources can downloaded by clicking here.

E-KSP

The prototype prover for E-connections between normal modal logics is based on KSP and deals with the global satisfiability problem for connected logics. The prover was implemented by Lucas de Moura Amaral as part of his Master's dissertation (A resolution-based E-connected calculus, 2019), which I have supervised. The sources can downloaded by clicking here.

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: