Elaine Gouvêa Pimentel

Pós-doutorado

Idiomas

Áreas de atuação

Organização de eventos

Participação em eventos

Participação em bancas

Orientou

Produções bibliográficas

• PEREIRA, LUIZ CARLOS ; Pimentel, Elaine ; DE PAIVA, VALERIA . Translations and Prawitz?s Ecumenical System. Studia Logica , v. 1, p. 1-16, 2024.

• OLARTE, CARLOS ; Pimentel, Elaine ; ROCHA, CAMILO . A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems. Journal of Logical and Algebraic Methods in Programming , v. 130, p. 100827, 2023.

• BLAISDELL, EBEN ; KANOVICH, MAX ; KUZNETSOV, STEPAN L. ; Pimentel, Elaine ; SCEDROV, ANDRE . Explorations in Subexponential Non-associative Non-commutative Linear Logic. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE , v. 381, p. 4-19, 2023.

• MARIN, SONIA ; Miller, Dale ; Pimentel, Elaine ; VOLPE, MARCO . From axioms to synthetic inference rules via focusing. ANNALS OF PURE AND APPLIED LOGIC , v. 173, p. 103091, 2022.

• XAVIER, BRUNO ; OLARTE, CARLOS ; Pimentel, Elaine . A linear logic framework for multimodal logics. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE , v. 32, p. 1176-1204, 2022.

• OLARTE, CARLOS ; Pimentel, Elaine ; XAVIER, BRUNO . A Fresh View of Linear Logic as a Logical Framework. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 351, p. 143-165, 2020.

• DALMONTE, TIZIANO ; Lellmann, Björn ; OLIVETTI, NICOLA ; Pimentel, Elaine . Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity. JOURNAL OF LOGIC AND COMPUTATION , v. 31, p. 67-111, 2020.

• CHAUDHURI, K. ; DESPEYROUX, J. ; OLARTE, C. ; PIMENTEL, E. . Hybrid linear logic, revisited. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE , v. 29, p. 1151-1176, 2019.

• Lellmann, Björn ; PIMENTEL, E. . Modularisation of Sequent Calculi for Normal and Non-normal Modalities. ACM Transactions on Computational Logic , v. 20, p. 1-46, 2019.

• Pimentel, Elaine ; PEREIRA, LUIZ CARLOS ; DE PAIVA, VALERIA . An ecumenical notion of entailment. SYNTHESE , v. 198, p. 5391-5413, 2019.

• OLARTE, C. ; PIMENTEL, E. ; RUEDA, C. . A concurrent constraint programming interpretation of access permissions. THEORY AND PRACTICE OF LOGIC PROGRAMMING , v. 18, p. 252-295, 2018.

• NIGAM, V. ; OLARTE, C. ; PIMENTEL, E. . On subexponentials, focusing and modalities in concurrent systems. THEORETICAL COMPUTER SCIENCE , v. 693, p. 35-58, 2017.

• OLARTE, CARLOS ; Pimentel, Elaine . On concurrent behaviors and focusing in linear logic. THEORETICAL COMPUTER SCIENCE , v. 685, p. 46-64, 2017.

• DESPEYROUX, JO?LLE ; OLARTE, CARLOS ; Pimentel, Elaine . Hybrid and Subexponential Linear Logics. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 332, p. 95-111, 2017.

• CIABATTONI, AGATA ; LELLMANN, BJ?RN ; OLARTE, CARLOS ; Pimentel, Elaine . From Cut-free Calculi to Automated Deduction: The Case of Bounded Contraction. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 332, p. 75-93, 2017.

• PIMENTEL, E. ; NIGAM, V. ; NETO, JOÃO . Multi-focused Proofs with Different Polarity Assignments. Electronic Notes in Theoretical Computer Science , v. 323, p. 163-179, 2016.

• OLARTE, C. ; PIMENTEL, E. . Proving Concurrent Constraint Programming Correct, Revisited. Electronic Notes in Theoretical Computer Science , v. 312, p. 179-195, 2015.

• OLARTE, C. ; PIMENTEL, E. ; NIGAM, V. . Subexponential concurrent constraint programming. THEORETICAL COMPUTER SCIENCE , v. 606, p. 98-120, 2015.

• NIGAM, V. ; PIMENTEL, E. ; OLARTE, C. . Dynamic Spaces in Concurrent Constraint Programming. Electronic Notes in Theoretical Computer Science , v. 305, p. 103-121, 2014.

• NIGAM, V. ; PIMENTEL, E. ; REIS, G. . An extended framework for specifying and reasoning about proof systems. Journal of Logic and Computation (Print) , v. 26, p. 539-576, 2014.

• Pimentel, Elaine ; OLARTE, CARLOS ; NIGAM, VIVEK . A Proof Theoretic Study of Soft Concurrent Constraint Programming. Theory and Practice of Logic Programming , v. 14, p. 649-663, 2014.

• MILLER, D. ; PIMENTEL, E. . A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science , v. 474, p. 98-116, 2013.

• PIMENTEL, E. ; RONCHI DELLA ROCCA, S. ; ROVERSI, L. . Intersection Types from a proof-theoretic perspective. FUNDAMENTA INFORMATICAE , v. 121, p. 253-274, 2012.

• Paolini, Luca ; PIMENTEL, E. ; RONCHI DELLA ROCCA, S. . Strong normalization from an unusual point of view. THEORETICAL COMPUTER SCIENCE , v. 412, p. 1903-1915, 2011.

• PIMENTEL, E. ; NIGAM, V. ; REIS, G. . Specifying Proof Systems in Linear Logic with Subexponentials. Electronic Notes in Theoretical Computer Science , v. 269, p. 109-123, 2011.

• PIMENTEL, E. ; PAOLINI, L. ; RONCHI DELLA ROCCA, S. . Lazy Strong Normalization. Electronic Notes in Theoretical Computer Science , v. 136, p. 103-116, 2005.

• KLIN, B. ; PIMENTEL, E. . 31st EACSL Annual Conference on Computer Science Logic (CSL). 1. ed. , 2023.

• CIABATTONI, A. ; PIMENTEL, E. . Logic, Language, Information, and Computation - 28th International Workshop, WoLLIC 2022. 1. ed. Springer, 2022. v. 13468.

• PIMENTEL, E. ; AYALA, M. (Org.) ; Kamareddine, F. (Org.) . Theoretical Computer Science. 37. ed. New York: Elsevier, 2011. v. 01. 115p .

• PIMENTEL, E. ; Benevides, M. (Org.) . Electronic Notes in Theoretical Computer Science. , 2009. v. 01. 156p .

• PIMENTEL, E. ; FIGUEIREDO, L. (Org.) ; QUEIROZ, R. (Org.) . WoLLIC´2003 - Proceedings. , 2003. v. 01. 225p .

• PEREIRA, LUIZ CARLOS ; Pimentel, Elaine . On an Ecumenical Natural Deduction with Stoup. Part I: The Propositional Case. In: Antonio Piccolomini d'Aragona. (Org.). Synthese Library. 1ed.: Springer International Publishing, 2024, v. 481, p. 139-169.

• PIMENTEL, E. ; MILLER, D. . Linear logic as a framework for specifying sequent calculus. In: Van Eijck;Oostrom;Visser. (Org.). Lecture Notes in Logic. 1ed.: Association for Symbolic Logic, 2004, v. 17, p. 111-135.

• FREIMAN, ROBERT ; OLARTE, CARLOS ; Pimentel, Elaine ; FERMÜLLER, CHRISTIAN . Reasoning About Group Polarization: From Semantic Games to Sequent Systems. In: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2024, Balaclava, 2024. v. 100. p. 70-87.

• PIMENTEL, E. ; PEREIRA, L. C. . A Tour on Ecumenical Systems (Invited Talk). In: Conference on Algebra and Coalgebra in Computer Science (CALCO), 2023. 10th Conference on Algebra and Coalgebra in Computer Science, {CALCO, 2023. v. 270. p. 3:1-3:15.

• PIMENTEL, E. ; BLAISDELL, E. ; KANOVICH, M. ; KUZNETSOV, S. ; SCEDROV, A. . Non-associative, Non-commutative Multi-modal Linear Logic. In: Automated Reasoning - 11th International Joint Conferencen (IJCAR), 2022, Haifa. Lecture Notes in Computer Science. Berlin: Springer, 2022. v. 13385. p. 449-467.

• PIMENTEL, E. ; OLARTE, C. ; NIGAM, V. . Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk). In: FSCD2021: 6th International Conference on Formal Structures for Computation and Deduction, 2021, Buenos Aires. Proceedingds of the 6th International Conference on Formal Structures for Computation and Deduction. Berlin: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. v. 195. p. 3:1-3:21.

• MARIN, S. ; PEREIRA, L. C. ; PIMENTEL, E. ; SALES, E. . A Pure View of Ecumenical Modalities. In: Logic, Language, Information, and Computation (WoLLIC), 2021, Lima. Lecture Notes in Computer Science, 2021. v. 13038. p. 388-407.

• DALMONTE, T. ; LELMANNN, B. ; OLIVETTI, N. ; PIMENTEL, E. . Countermodel Construction via Optimal Hypersequent Calculi for Non-normal Modal Logics. In: Logical Foundations of Computer Science - International Symposium (LFCS 2020), 2020, Deerfield Beach. Lecture Notes in Computer Science. New York: Springer, 2020. v. 11972. p. 27-46.

• Pimentel, Elaine . Proof systems for Geometric theories (PROGEO). In: Workshop Brasileiro de Lógica, 2020, Brasil. Anais do Workshop Brasileiro de Lógica (WBL 2020), 2020. p. 57-64.

• MARIN, S. ; PEREIRA, L. C. ; PIMENTEL, E. ; SALES, E. . Ecumenical Modal Logic. In: International Workshop on Dynamic Logic, 2020, Praga. Dynamic Logic. New Trends and Applications. Berlin: Springer, 2020. v. 12569. p. 187-204.

• PIMENTEL, E. ; LELMANNN, B. ; RAMANAYAKE, R. . Sequentialising Nested Systems. In: TABLEAUX 2019 (28th Automated Reasoning with Analytic Tableaux and Related Methods), 2019, Londres. Lecture Notes in Computer Science. Berlin: Springer, 2019. v. 11714. p. 147-165.

• LANG, T. ; OLARTE, C. ; PIMENTEL, E. ; FERMULLER, C. . A Game Model for Proofs with Costs. In: TABLEAUX 2019 (28th Automated Reasoning with Analytic Tableaux and Related Methods), 2019, Londres. Lecture Notes in Computer Science. Berlin: Springer, 2019. v. 11714. p. 241-258.

• PIMENTEL, E. . A Semantical View of Proof Systems. In: WoLLIC: International Workshop on Logic, Language, Information, and Computation, 2018, Bogotá. Lecture Notes in Computer Science. Berlin: Springer, Berlin, Heidelberg, 2018. v. 10944. p. 61-76.

• OLARTE, C. ; PIMENTEL, E. ; ROCHA, C. . Proving Structural Properties of Sequent Systems in Rewriting Logic. In: WRLA 2018 - 12th International Workshop on Rewriting Logic and Its Applications, 2018, Thessaloniki. Lecture Notes in Computer Science. New York: Springer, 2018. v. 11152. p. 115-135.

• OLARTE, C. ; PAIVA, V. ; PIMENTEL, E. ; REIS, G. . The ILLTP Library for Intuitionistic Linear Logic. In: Joint International Workshop on Linearity & Trends in Linear Logic and Applications, 2018, Oxford. Electronic Proceedings of Theoretical Computer Science, 2018. v. 292. p. 118-132.

• LELMANNN, B. ; OLARTE, C. ; PIMENTEL, E. . A uniform framework for substructural logics with modalities. In: LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017, Maun. LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017. v. 46. p. 435-455.

• PIMENTEL, E. ; Lellmann, Björn . Automatic generation of focused proof systems. In: Escola de Informática Teórica e Métodos Formais, 2016, Natal. Anais - Escola de Informática Teórica e Métodos Formais, 2016. p. 105-109.

• LELMANNN, B. ; PIMENTEL, E. . Proof Search in Nested Sequent Calculi. In: 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-20), 2015, Suva - Fiji. Lecture Notes in Computer Science, 2015. v. 9450. p. 558-574.

• NIGAM, V. ; OLARTE, C. ; PIMENTEL, E. . A General Proof System for Modalities in Concurrent Constraint Programming. In: 24th International Conference on Concurrency Theory (CONCUR'13), 2013, Buenos Aires. LNCS. Berlin: Springer-Verlag, 2013. v. 8052.

• OLARTE, CARLOS ; NIGAM, V. ; PIMENTEL, E. . Subexponentials in Concurrent Constraint Programming. In: 8th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2013), 2013, São Paulo. 8th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2013), 2013.

• OLARTE, CARLOS ; Pimentel, Elaine ; RUEDA, CAMILO ; CATAÑO, NESTOR . A linear concurrent constraint approach for the automatic verification of access permissions. In: the 14th symposium, 2012, Leuven. Proceedings of the 14th symposium on Principles and practice of declarative programming - PPDP '12. New York: ACM Press. p. 207-216.

• PIMENTEL, E. ; REIS, G. . Using Linear Logic with Subexponentials to Implement Logic Interpreters. In: Simpósio Brasileiro de Métodos Formais (SBMF), 2010, Natal. Proceedings of SBMF, 2010.

• PIMENTEL, E. ; Fernandes, I. ; RODRIGUES, C. F. ; Leal, W. ; Luiz, W. . PLLIC - Provador para as lógicas linear, intuicionista e clássica. In: LAPTEC, 2007, Santos. LAPTEC, 2007.

• PAOLINI, L. ; PIMENTEL, E. ; RONCHI DELLA ROCCA, S. . An Operational Characterization of Strong Normalization. In: Foundations of Software Science and Computation Structures (FOSSACS 2006), 2006, Viena. Lecture Notes in Computer Science, 2006. v. 3921. p. 367-381.

• PIMENTEL, E. ; RONCHI DELLA ROCCA, S. ; ROVERSI, L. . Intersection Types: a Proof-Theoretical Approach. In: Structures and Deduction'05 - ICALP, 2005, Lisboa. Proceedings of SD'05 - associated to ICALP, 2005.

• PIMENTEL, E. ; MILLER, D. . On the Specification of Sequent Systems. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005), 2005, Montego Bay. Lecture Notes in Computer Science, 2005. v. 3835. p. 352-366.

• MILLER, D. ; PIMENTEL, E. . Using Linear Logic to Reason about Sequent Systems. In: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2012), 2002, Copenhagen. Lecture Notes in Computer Science, 2002. v. 2381. p. 2-23.

• PIMENTEL, E. ; MILLER, D. . Towards a logical framework for sequent calculus. In: Natural Deduction Meeting, 2001, Rio de Janeiro. Proceedings of Natural Deduction meeting, 2001.

• PIMENTEL, E. ; FIGUEIREDO, C. C. ; FIGUEIREDO, L. . Tipos em Linguagens de Programação. In: III Simpósio Brasileiro de Linguagens de programação, 1999, Porto Alegre. Anais do III Simpósio Brasileiro de Linguagens da Programação, 1999.

• PIMENTEL, E. ; MILLER, D. . On the Specification of Sequent Systems. In: XIV Latin American Symposium on Mathematical Logic (SLALM), 2009, Paraty. The Bulletin of Symbolic Logic, 2009. v. 15. p. 364-364.

• PIMENTEL, E. ; MARIN, S. . Focusing, axioms and synthetic inference rules (invited speaker). 2020. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. . A fresh view of linear logic as a logical framework (invited speaker). 2020. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. . Lógica Matemática e Axiomas Geométricos (palestrante convidada). 2020. (Apresentação de Trabalho/Conferência ou palestra).

• PIMENTEL, E. . A Game Model for Proofs with Costs. 2020. (Apresentação de Trabalho/Seminário).

• PIMENTEL, E. . Modalities as prices: a game model of intuitionistic linear logic with subexponentials. 2020. (Apresentação de Trabalho/Seminário).

• PIMENTEL, E. . Trying to understand resource consciousness. 2020. (Apresentação de Trabalho/Seminário).

• PIMENTEL, E. . Ecumenical modalities. 2020. (Apresentação de Trabalho/Seminário).

• PIMENTEL, E. ; RAMANAYAKE, R. ; LELMANNN, B. . Sequentialising nested systems. 2019. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. ; RAMANAYAKE, R. ; LELMANNN, B. . Sequentialising nested systems (invited speaker). 2019. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. ; PEREIRA, L. C. ; PAIVA, V. . An ecumenical notion of entailment (invited speaker). 2019. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. ; OLARTE, C. ; LANG, T. ; FERMULLER, C. . Modalities as prices: a game model of intuitionistic linear logic with subexponentials (invited speaker). 2019. (Apresentação de Trabalho/Simpósio).

• PIMENTEL, E. . Logic, modalities and computation. 2018. (Apresentação de Trabalho/Conferência ou palestra).

• PIMENTEL, E. . A semantical view of proof systems. 2018. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. . A unified view of modal and substructural logics. 2016. (Apresentação de Trabalho/Conferência ou palestra).

• PIMENTEL, E. . Onthe universality of proofs. 2016. (Apresentação de Trabalho/Conferência ou palestra).

• PIMENTEL, E. ; OLARTE, CARLOS ; NIGAM, V. ; Miller, Dale ; REIS, G. . On modalities and linearity. 2014. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. ; OLARTE, CARLOS ; NIGAM, V. ; Miller, Dale ; KESNER, D. . On modalities, focusing, harmony, concurrency and polarized lambda-calculus. 2014. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. ; OLARTE, CARLOS . Proving concurrent constraint programming correct, revisited. 2014. (Apresentação de Trabalho/Congresso).

• PIMENTEL, E. ; BENEVIDES, MARIO . Proceedings of the 6th Workshop on Intuitionistic Modal Logic and Applications (IMLA), 2013., 2014. (Prefácio, Pósfacio/Prefácio)>.

• NIGAM, V. ; PIMENTEL, E. ; REIS, G. . An Extended Framework for Specifying and Reasoning about Proof Systems 2012 (Relatório Técnico).

• AYALA, M. ; PIMENTEL, E. ; Kamareddine, F. . Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications, 2011, 2011. (Prefácio, Pósfacio/Prefácio)>.

• PIMENTEL, E. ; VENNERI, B. ; WELLS, J. . Proceedings Fifth Workshop on Intersection Types and Related Systems, ITRS 2010, 2010. (Prefácio, Pósfacio/Prefácio)>.

• PIMENTEL, E. ; RODRIGUES, C. F. ; Fernandes, I. ; Luiz, W. ; Leal, W. . PLLIC: provador para as lógicas linear, intuicionista e clássica 2007 (Relatório Técnico).

• PIMENTEL, E. ; SILVA, M. L. . Semântica operacional estruturada. Ouro Preto: UFOP, 1999 (Relatório Técnico).

Outras produções

Projetos de pesquisa

• 2020 - Atual

  Lógicas Ecumênicas, Descrição: Com a variedade de assistentes de prova e provadores automáticos de teoremas baseados em diferentes sistemas formais, é interessante descobrir qual parte de uma prova produzida (semi-)automaticamente depende do raciocínio clássico ou quando permanece no mundo construtivo/intuicionista. De fato, esse é um passo fundamental para a mobilidade de provas entre diferentes sistemas computacionais. Neste projeto de pesquisa, pretendemos propor um arcabouço {\em ecumênico} para fornecer uma visão uniforme de sistemas clássicos e intuicionistas, utilizando-o para realizar um estudo formal de comportamentos construtivos e não-construtivos em geral (incluindo modalidades). Ao propor sistemas simples onde o clássico e intuicionista convivem em harmonia, estamos abrindo a possibilidade de refletir, de maneira pontual e fiel, usos "locais" para raciocínio não construtivo. Além disso, uma visão ecumênica de sistemas pode abrir caminho para uma interpretação categórica e, consequentemente, uma interpretação computacional do arcabouço proposto (via um sistema de tipos ecumênico).. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (10) / Mestrado acadêmico: (1) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Carlos Olarte - Integrante / Luiz Carlos Pereira - Integrante / Sonia Marin - Integrante / Emerson Sales - Integrante.

• 2020 - Atual

  PROGEO: Proof systems for Geometric theories, Descrição: Dentro do espectro de lógicas polarizadas, bipoles são fórmulas que possuem uma forma particular: conectivos externos positivos que requerem alguma decisão em uma derivação (eg, escolhendo substituições adequadas em quantificadores existenciais) e conectivos internos negativos, que podem ser decompostos em uma derivação sem mudar a demonstrabilidade. Na disciplina de focusing, fórmulas negativas são decompostas avidamente até que apenas fórmulas positivas restem; então, uma delas é escolhida não-deterministicamente para ser focada. Se esta fórmula é um bipole, ela vai ser completamente decomposta em um passo de derivação focado. Interpretando regras de inferência da lógica-objeto como bipoles, focusing força uma correspondência 1-1 entre a aplicação de regras e a derivação de fórmulas. Por outro lado, o interesse no estudo de teorias geométricas aparece em diversas áreas de lógica, matemática e computação teórica, tais como topologia, geometria, teoria de categorias e lógicas modais. A ideia principal deste projeto é adicionar teorias determinadas por axiomas geométricos à lógica de primeira ordem. A nossa ideia é utilizar bipoles e focusing para estabelecer um método sistemático para transformar tais axiomas em regras, de modo que a extensão do sistema inicial com tais regras seja suave, ie, mantendo as meta-propriedades do sistema original, tais como analiticidade.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Dale Miller - Integrante / Carlos Olarte - Integrante / Luiz Carlos Pereira - Integrante / Sonia Marin - Integrante / Marco Volpe - Integrante.

• 2020 - Atual

  MOSAIC - Modalities in Substructural Logics: Theory, Methods and Applications, Descrição: Modal logic is an area of research introduced around one century ago to address the philosophical issues of reasoning about the ?modes of truth?. Nowadays, more than just being a field of research in logic, modal logic can be rather regarded as a methodological framework aimed at providing formal tools to capture a plethora of modes of truth: in tense (or temporal) logic, modalities are interpreted as ?earlier? or ?eventually?; deontic logics formalize what is ?permitted? or ?obligatory?; epistemic logic concern what agents ?know?, ?believe? or ?consider plausible? in a given situation; land so forth. The aim of the present proposal is to put forward a systematic study of substructural modal logics, understood as those modal logics in which the modal operators are based upon the more general ground of substructural logics. The latter are weaker deductive systems than classical logic, defined by removing some of the structural rules in Gentzen sequent calculi for classical logic. Recently, several communities started being involved in the area of substructural modal logics, causing a momentous growth which precisely now calls for unifying perspectives. The main aim of this proposal is hence to develop a comprehensive theory in which substructural modal logics are studied as a family and not in isolation, and to systematically integrate the proof-theoretic, the algebraic and the relational semantic perspectives on these logics so as to create a lingua franca which will facilitate the transfer of results and insights among communities of logicians, and will also help to establish new and unexpected connections between different fields of application.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Elaine Gouvêa Pimentel - Integrante / Carlos Olarte - Integrante / João Marcos Almeida - Integrante / Umberto Rivieccio - Coordenador.

• 2019 - 2022

  PROSA - PROof search for Substructural and modAl logics, Descrição: PROJETO UNIVERSAL - CNPq (2019--2021) Este projeto visa aprimorar o estado da arte de teoria da prova para lógicas que são variantes ou generalizações de lógicas sub-estruturais e/ou modais. Mais especificamente, pretendemos propor cálculos analíticos e métodos de busca por provas eficientes para uma classe representativa de lógicas modais e sub-estruturais. Além disso, pretendemos conciliar a visão sintática/semântica de maneira natural e direta, ao mesmo tempo estabelecendo uma contra-partida computacional para as lógicas consideradas. Por fim, pretendemos propor arcabouços lógicos adequados para a especificação de propriedades de sistemas lógicos de maneira uniforme. Isso deve permitir não apenas uma validação experimental dos resultados teóricos, mas também o desenvolvimento de protótipos de implementação para vários cálculos mencionados neste projeto.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (1) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Dale Miller - Integrante / Carlos Olarte - Integrante / João Marcos Almeida - Integrante / Luiz Carlos Pereira - Integrante / Delia Kesner - Integrante / Agata Ciabattoni - Integrante / Björn Lelmannn - Integrante / Camilo Rocha - Integrante / Umberto Rivieccio - Integrante / Revantha Ramanayake - Integrante / Kaustuv Chaudhuri - Integrante / Valeria de Paiva - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.

• 2019 - Atual

  Rewriting Logic as a framework for specifying sequent systems, Descrição: General and effective methods are required for providing good automation strategies to prove properties of sequent systems. Structural properties such as admissibility, invertibility, and permutability of rules are crucial in proof theory, and they can be used for proving other key properties such as cut-elimination. However, finding proofs for these properties requires inductive reasoning over the provability relation, which is often quite elaborated, exponentially exhaustive, and error prone. This project aims at developing automatic techniques for proving structural properties of sequent based systems. The proposed techniques will be presented in the rewriting logic metalogical framework, and use rewrite- and narrowing-based reasoning.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (4) / Mestrado acadêmico: (1) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Carlos Olarte - Integrante / Camilo Rocha - Integrante.

• 2017 - 2020

  Busca por provas em lógicas modais e sub-estruturais, Descrição: PROJETO PQ-CNPq (2017-2019) Este projeto visa propor sistemas de provas baseados em sequentes aninhados para lógicas modais que estendem tanto a lógica clássica proposicional quanto a lógica linear. Apresentando sistemas modulares, tornaremos possível propor provadores de teoremas para tais lógicas de maneira uniforme, o que possibilita também a verificação de propriedades para os sistemas abordados.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (10) / Mestrado acadêmico: (4) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Dale Miller - Integrante / Carlos Olarte - Integrante / Agata Ciabattoni - Integrante / Björn Lelmannn - Integrante / Roman Kuznets - Integrante / Revantha Ramanayake - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.

• 2017 - 2019

  STIC AmSud/CAPES -- Projeto EPIC (EPistemic Interactive Concurrency), Projeto certificado pelo(a) coordenador(a) Carlos Alberto Olarte Vega em 17/01/2017., Descrição: Giving mathematical foundations to today?s concurrent systems (i.e., computational systems of multiple agents that interact with each other) is a serious challenge for theoretical computer science. Traditional mathematical models from concurrency theory do not single out two fundamental aspects of these systems: namely, epistemic and spatial behavior.In this project we take up the task of developing a mathematical model, conceptually different from existing models of concurrency, for the precise understanding of epistemic and spatial behavior in today?s concurrent systems. The model will be able to rigorously predict the behavior of a concurrent system in the presence of complex flow of epistemic information such as knowledge, facts, public announcements, lies and opinions. A compelling application of the model will be to predict if in a given social network, certain intentional lie may lead to unwanted situations such as the public announcement of sensitive information or other intrusive behaviors.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (10) / Mestrado acadêmico: (5) / Doutorado: (2) . , Integrantes: Elaine Gouvêa Pimentel - Integrante / Miller, Dale - Integrante / OLARTE, CARLOS - Coordenador / RUEDA, CAMILO - Integrante / Catuscia Palamidessi - Integrante / Mario Sergio Alvim - Integrante / Camilo Rocha - Integrante / Frank Valencia - Integrante., Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro / Departamento Administrativo de Ciencia, Tecnología e Innovación - Auxílio financeiro / Centre de Recherche Inria Saclay - Île-de-France - Auxílio financeiro.

• 2015 - 2017

  Programa CAPES/FAPERN, Descrição: APOIO AOS PROGRAMAS DE PÓS-GRADUAÇÃO DAS INSTITUIÇÕES DE ENSINO SUPERIOR (IES) DO ESTADO DO RIO GRANDE DO NORTE. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (10) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Dione Valença - Integrante / Andre Pinho - Integrante / André Campos - Integrante / Sidarta Araújo - Integrante., Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro.

• 2014 - 2017

  MUSICAL - MUsic and Spatial Interaction with Constraints, Algebra and Logic: foundations and applications, Descrição: This multi-disciplinary project aims to the development and integration of tools from logic and con- currency theory for the design and analysis of reactive systems [SJG96] and to their application to musical processes and multimedia systems. The target framework is a variant of tcc, a temporal extension of concurrent constraint programming (CCP) [Sar93] which unifies in a single declarative style the logical and the behavioral specification of temporal processes. In order to take into account the location and mobility of these processes we propose to extend tcc to integrate the specification of spatial relationships between themselves, using for this linear logic with subexponentials. This type of formalism is relevant for the specification and the analysis of emerging applications with advanced interaction with their environment and their users such as those in ubiquitous comput- ing, mobile systems, and multimedia interacting systems. Indeed, these applications require all the description of dynamic and temporized interactions between autonomous localized entities (users, agents, or processes). Besides developing the necessary theory, using linear logic with subexponentials, for handling space-time agents, we propose to apply these theoretical tools to three types of problems originated in music applications: (a) real-time interaction during performance, (b) specification of high level sound spatialization processes and (c), dynamic spatial representation of symbolic musical objects. These applications require the expression of complex coupled spatial and temporal constraints in a real-time environment, which will be an excellent framework to validate the expressiveness and effectiveness of the tools. Finally, we also intend to add to linear logic the notion of probability which is central in the model- ing of musical systems that react according to the laws of probability rather than non-deterministically (for instance in music improvisation systems). As far as we know, probabilistic notions has been introduced in CCP calculi but the connection to logic (for verification purposes) has not been studied for those variants.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (4) / Mestrado acadêmico: (1) / Doutorado: (4) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Carlos Olarte - Integrante / Camilo Rueda - Integrante.

• 2013 - 2016

  Uma estrutura lógica para sistemas concorrentes epistêmicos, temporais e espaciais, Descrição: A programação concorrente com restrições (ccp) é um formalismo atrelado à lógica simples e poderoso. Diversas extensões do modelo têm sido propostas para lidar com noções tais como tempo e não-determinismo para sistemas reativos, comportamento probabilístico, linearidade de recursos e mobilidade, por exemplo. Por outro lado, a lógica linear é um formalismo bem conhecido para especificar e verificar sistemas lógicos e computacionais. Recentemente, subexponenciais em lógica linear (SELL) têm sido utilizados para especificar uma quantidade maior de tais sistemas. A idéia principal deste projeto é propor uma extensão de SELL que permita quantificação sobre subexponenciais (que chamaremos SELLU) como formalismo único para descrever uma gama de sistemas baseados em ccp e, deste modo, unificar diversas abordagens existentes. Por outro lado, pretendemos utilizar todo o poder de especificação/verificação de SELLU para diversificar o espectro de sistemas concorrentes que podem ser especificados no cálculo e, ao mesmo tempo, preservar o aspecto declarativo de processos como fórmulas, aumentando assim a expressividade de ccp. Por fim, pretendemos implementar todo o ferramental teórico e aplicar a robustez de SELLU para a verificação de propriedades em sistemas concorrentes em diferentes cenários, como computação orientada a serviços, sistemas distribuídos e interações bioquímicas.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (5) / Mestrado acadêmico: (2) / Doutorado: (1) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Vivek Nigam - Integrante / Carlos Olarte - Integrante / Camilo Rueda - Integrante / David Deharbe - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.

• 2013 - 2016

  GeVe Generalizações de Verofuncionalidade, Descrição: O projeto GeVe trata do estudo de várias formas bem motivadas através das quais as propri- edades e metapropriedades mais atraentes das lógicas verofuncionais podem ser alargadas de modo a cobrir terrenos lógicos mais amplos. A ubiquidade do uso das lógicas não-clássicas na formalização do raciocínio prático exige a formulação de teorias do significado e da com- posicionalidade mais flexíveis do que as usuais, teorias estas que permitam o estabelecimento de bases mais inclusivas para a compreensão de tais lógicas. Tais investigações pressupõem não apenas o desenvolvimento de arcabouços adequados desde as perspectivas da Teoria dos Modelos, da Teoria das Demonstrações e da Lógica Universal, mas também a construção de pontes sólidas entre estes campos de estudo, baseadas em diversas generalizações da noção de verofuncionalidade. Para as lógicas verofuncionais neste sentido ampliado, em suas múltiplas versões, prevêem-se aplicações em diversas áreas da ciência da computação, da matemática, da filosofia e da linguística, onde a complexidade sempre crescente dos sistemas erigidos dá origem a novos e complicados desafios para a composicionalidade.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Elaine Gouvêa Pimentel - Integrante / Edward Hernann Haeusler - Integrante / Vivek Nigam - Integrante / Regivan Santiago - Integrante / João Marcos Almeida - Coordenador / Luiz Carlos Pereira - Integrante / Benjamín René Callejas Bedregal - Integrante / Alexandre Rademaker - Integrante / Jean-Yves Beziau - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.

• 2013 - 2016

  Provas: identidade, estrutura e representação ? PIER, Descrição: A Teoria Geral da Prova é o ramo da Lógica que investiga o conceito de prova em todos os seus aspectos e, em particular, a estrutura de provas formais. A Te- oria da Prova é uma área naturalmente multidisciplinar, contemplando pesquisas nas áreas da Filosofia, da Matemática e da Ciência da Computação. Apesar dos importantes resultados já obtidos em pesquisas em Teoria da Prova nos últimos oitenta anos, existem ainda muitas questões em aberto, para as quais novos de- senvolvimentos nessa área multidisciplinar podem ajudar a responder, mesmo que parcialmente. Uma das questões centrais é certamente a questão da definição de um critério de identidade para provas. Neste projeto, abordaremos o problema da identidade de provas a partir dessa perspectiva multidisciplinar, investigando aspectos filosóficos, matemáticos e computacionais dessa importante questão.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Elaine Gouvêa Pimentel - Integrante / Edward Hernann Haeusler - Integrante / Vivek Nigam - Integrante / Luiz Carlos Pereira - Coordenador / Wagner Sanz - Integrante / Gisele Secco - Integrante / Abell Lassalle Casanave - Integrante / Jean Baptiste Joinet - Integrante / Veleria de Paiva - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.

• 2012 - 2016

  GeTFun: Generalizing Truth-Functionality, Descrição: A coordinated exchange programme for the investigation of compositional meaning in logic and applications.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Elaine Gouvêa Pimentel - Integrante / João Marcos Almeida - Coordenador / Valéria de Paiva - Integrante / Agata Ciabattoni - Integrante / Björn Lelmannn - Integrante.

• 2010 - 2011

  Linear logic, focusing and the specification of logical systems, Descrição: Projeto financiado pela FAPEMIG e INRIA para cooperação internacional. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (4) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Dale Miller - Integrante.

• 2002 - 2016

  Lógica Linear e a especificação de sistemas lógicos e computacionais, Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) . , Integrantes: Elaine Gouvêa Pimentel - Coordenador / Dale Miller - Integrante., Financiador(es): Institut National de Recherche en Informatique et en Automatique - Siège - Cooperação / Universita degli studio di Torino - Outra / Ecole Polytechnique - Auxílio financeiro., Número de produções C, T & A: 8

Prêmios