I am a lecturer and researcher at the Computer Science Department at the University of Brasília.
Address: |
| 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 |
PhD in Computer Science - Department of Computer Science - University of Liverpool
MSc in Computer Science - Institute
of Computing - University of Campinas
BSc in Computer Science - Computer Science
Department - 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 between a linear-time temporal logics and multi-modal S5. This work was part of the EPSRC funded project Resolution-Based Theorem-Proving for Temporal Logics of Knowledge and Belief with Interactions. More recently, I have been working in collaboration with Dr. Clare Dixon, from the University of Liverpool, in a long-term project concerning the development of both theoretical issues and implementantion of tools for normal modal logics. My work in this project is currently funded by CNPq, the Brazilian Research Council (UNIVERSAL 471791/2004-0: Teoria Semântica, Lógica e Aplicações da Computação; CT-INFO 506598/04-7: Simulação Algorítmica, Semântica e Aplicações da Computação).
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
R. Schmidt, I. Pratt-Hartmann, M. Reynolds, and H. Wansing (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,
R. de Queiroz & M. Ayala-Rincon (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,
Flávio Moreira de Oliveira (Ed.), Advances in Artificial
Intelligence, Lecture Notes in Computer Science 1515 Springer 1998, pages 159-177.
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. M. V. Zelkowitz & P. Straub (eds.),
Valdivia, Nov. 1996, Sociedad Chilena de Ciencia de Computacion (SCCC),
1996.
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.