Edward Hermann Haeusler

possui graduação em Matemática pela Universidade de Brasília (1983), mestrado em Informática pela Pontifícia Universidade Católica do Rio de Janeiro (1986) e doutorado em Informática pela Pontifícia Universidade Católica do Rio de Janeiro (1990). Atualmente é professor associado da Pontifícia Universidade Católica do Rio de Janeiro. Tem experiência na área de Ciência da Computação, com ênfase em Computabilidade e Modelos de Computação, atuando principalmente nos seguintes temas: teoria da prova, proof theory, teoria das categorias, semântica formal e Lógica. Foi coordenador de Pós-Graduação do DI-PUC de 2010-2 a 2014-1. Estive como coordenador do PPG-Informática da PUC-Rio desde Maio/2023 até Março/2024

Informações coletadas do Lattes em 26/07/2025

Acadêmico

Formação acadêmica

Doutorado em Informática

1986 - 1990

Pontifícia Universidade Católica do Rio de Janeiro, PUC-Rio
Título: Prova Automática de Teoremas em Dedução Natural : Uma Abordagem Abstrata
, Ano de obtenção: 1990. Tarcísio Haroldo Cavalcanti Pequeno. Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.

Mestrado em Informática

1984 - 1986

Pontifícia Universidade Católica do Rio de Janeiro, PUC-Rio
Título: Prova Automática de Teoremas: Uma abordagem para melhorar a legibilidade de provas baseada em Dedução Natural, Ano de Obtenção: 1986
Paulo Augusto Silva Veloso.Grande área: Ciências Exatas e da Terra

Graduação em Matemática

1979 - 1983

Universidade de Brasília, UnB

Pós-doutorado

2013 - 2014

Pós-Doutorado. , Institut National de Recherche en Informatique et en Automatique - Siège, INRIA, França. , Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil. , Grande área: Ciências Exatas e da Terra

2003 - 2003

Pós-Doutorado. , Eberhard Karls Universitãt Tuebingen, EKUT, Alemanha. , Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil. , Grande área: Ciências Exatas e da Terra

1994 - 1994

Pós-Doutorado. , Aarhus University, AU, Dinamarca. , Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil.

Idiomas

Inglês

Fala Bem, Lê Bem, Escreve Bem.

Alemão

Fala Pouco, Lê Pouco, Escreve Pouco.

Áreas de atuação

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Computabilidade e Modelos de Computação.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Lógicas e Semântica de Programas.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Linguagem Formais e Autômatos.

Organização de eventos

AYALA-RINCÓN, M. ; HAEUSLER, E. H. . TLCA - Types, Lambda Calculus and Applications. 2009. (Congresso).

HAEUSLER, E. H. . Simpósio Brasileiro de Linguagens de Programação. 2002. (Congresso).

HAEUSLER, E. H. . Workshop de Métodos Formais. 2001. (Congresso).

PEREIRA, L. C. ; HAEUSLER, E. H. ; PAIVA, V. . Natural Deduction 2000. 2000. (Congresso).

Participação em eventos

DaLí - Dynamic Logic: new trends and applications (workshop of Tableaux2017).Propositional Dynamic Logic with Petri net programs: A discussion and a logical system. 2017. (Simpósio).

Encontro Brasileiro de Lógica. Proof Compression, The Conjectures NP vs PSPACE and NP vs coNP.. 2017. (Congresso).

Fisrt Workshop on Foundations of Mathematics.Compression of propositional proofs. On proof-theoretical arguments in favor of the conjectures NP=CoNP and NP=PSPACE.. 2017. (Oficina).

TABLEAUX2017 - The 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods.Tutorial on Proof compressions and the conjecture NP = PSPACE (6 hours). 2017. (Simpósio).

XXI Colóquio Conesul de Filosofia das Ciências Formais.Mesa Redonda: Derivações, provas e argumentos: alguns aspectos (Joint with P. Veloso and J-B Joinet). 2017. (Simpósio).

XX Colóquio Conesul de Filosofia das Ciências Formais.Solving Problems in Intuitionistic Type Theory via General Problem Theory. 2016. (Simpósio).

WEIT - Workshop Escola de Informática Teórica.Finito não-padrão e Computação Formal. 2015. (Seminário).

XIX Colóquio Conesul de Filosofia das Ciências Formais.Computational Manifolds and Sheaves. 2015. (Simpósio).

Contest for the Universal Logic Prize.First International Conference on Universal Logic. 2005. (Simpósio).

First Conference on Universal Logic.A short Course on Universal Computation (together with R.Lins de Carvalho e C. Macedo). 2005. (Simpósio).

Orientou

Pietro Ribeiro Pepe

Algorithmic Complexity Measure: a proposal based on Linear Bounded Automaton and Applications to Neuroscience; Início: 2024; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro; (Orientador);

Luis Henrique Costa Neto

A more detailed model of the elongation process in protein synthesis; Início: 2024; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro; (Orientador);

Lorenzo Saraiva

"Short proofs for non-Hamiltonian graphs through quantum computing: Implementation and Feasible Applications; Início: 2024; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; (Orientador);

Guilherme Felix da Silva

Assisted theorem proving for security protocols based on Sheaves; Início: 2018; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Fundacao de Amparo a Pesquisa do Exercito Brasileiro; (Orientador);

Cleyton Slaviero

Rationality in CS via Game Theory; Início: 2015; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro; (Orientador);

Felipe da Rocha Lopes

PAC Learning em uma abordagem de Predição de falhas em ativos de transmissão de energia; 2024; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Lorenzo Palermo Saraiva

Quantum algorithms for proof search in linear logic,; 2022; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Rodrigo Leite da Silva

Jogos para o aprendizado de programação: como as modalidades mono e multijogadores afetam a motivação; 2022; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

ROBINSON CALLOU DE MOURA BRASIL FILHO

Using LEAN to show that every exponentially big normal proof in Minimal Implicational Logic is exponentially redundant; 2019; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Bernardo Pinto de Alkmim

A Lógica sobre Leis iALC: Implementação de Provas de Correção e Completude e Proposta de Formalização da Legislação Brasileira; 2019; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

José Flávio Cavalcante Barros Júnior

Uma Abordagem Experimental sobre a Compressão de Provas em Dedução Natural Minimal Implicacional; 2019; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Guilherme Felix da Silva

Formalização de Algoritmos de Criptografia em um Assistente de Provas Interativo; 2018; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Vitor Pinheiro de Almeida

Contex in Ontologies; 2011; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Aleksander Medella Campos da Silva

Uma Biblioteca de Componentes De Software para Simuladores De Radar; 2011; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Coorientador: Edward Hermann Haeusler;

RENATO JAVIER MARROQUIN MOGROVEJO

Experimental Statistical Analysis of MapReduce Joins; 2011; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Coorientador: Edward Hermann Haeusler;

Luciana da Silva Almendra Gomes

Proveniência para Workflows de Bioinformática; 2011; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Coorientador: Edward Hermann Haeusler;

Jefferson Santos

Uma Infraestrutura WEB-Service para interfaces de provradores interativos de teoremas; 2010; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Cecíclia Englander Lustosa

On the 2-Categorial view of Proof Theory; 2009; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Bruno Schroeder

A Graph Based Theorem Proving Platform with Strategies; 2008; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Davi Romero Vasconcelos

Análise de Estratégias Utilizando Verificação Formal de Modelos; 2003; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Juliana Carpes Imperial

Técnicas para o Uso de Cálculo de Hoare em PCC; 2003; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Marcelo Jaccoud do Amaral

Mantendo Código Fonte em XML: Rumo ao Hiperfonte; 2001; 0 f; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Fernando Náufel do Amaral

Uma Lógica de Ações para Sistemas de Transição Temporizados; 2000; 0 f; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Carlos Bazílio Martins

Detecção de Paralelismo a partir da Semântica Denotacional e de Grafos de Dependências; 2000; 0 f; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Christian Renteria

CN: Dedução Natural para CLT; 2000; 0 f; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

[Nome removido após solicitação do usuário]

Um provador Interativo de Teoremas em Dedução Natural; 2000; 0 f; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Geiza Maria Hamazaki da Silva

Um Estudo em Síntese Construtiva de Programas Utilizando Lógica Intuicionista; 1999; 0 f; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Marcelo Fagundes Félix

Let : Uma Linguagem de Suporte A Transformacoes Em Alto Nivel; 1998; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Neudson Cavalcante Albuquerque

Prova Automática de Teoremas nas Fork Algebras; 1995; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Edward Hermann Haeusler;

Isabel Leite Cafezeiro

Um Prototipo Para Simulacao de Processos Em Csp: Um Enfoque Orientado A Objetos; 1994; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Adriana Carlos Paz

Um Ambiente para Prova Automática de Teoremas em Dedução Natural; 1993; Dissertação (Mestrado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

ROBINSON CALLOU DE MOURA BRASIL FILHO

Arguing NP = PSPACE: On the Coverage and Soundness of the Horizontal Compression Algorithm; 2024; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Fernando Antônio Dantas Gomes Pinto

Compliance Reasoning on Legal Norms: a logic-based approach; 2024; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Bernardo Alkmim

Law and Order(ing): Providing a Natural Deduction System and Non-monotonic Reasoning to an Intuitionistic Description Logic,; 2023; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Bruno Cuconato Claro

A labelled Natural Deduction Logical Framework,; 2023; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Jefferson de Barros Santos

Systems for Provability and Countermodel Generation in Propositional Minimal Implicational Logic; 2017; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Bruno Lopes Vieira

Extending Propositional Dynamic Logic for Petri Nets; 2014; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Marcela Quispe Cruz

Some Results in a Proof-theory Based on Graphs; 2014; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Cecília Englander Lustosa

On some relations between Natural Deduction and Sequent Calculus; 2014; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Cristian Tristão

Uma Abordagem para Modelar, Armazenar e Acessar Sequências Biológicas; 2012; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Coorientador: Edward Hermann Haeusler;

Ricardo Queiroz de Araújo Fernandes

Proximity-Based Understanding of Conditionals; 2012; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Alexandre Rademaker

On a Proof Theory for Description Logics; 2010; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Vaston Gonçalves da costa

Compactação de Provas Lógicas; 2007; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Davi Romero de Vasconcelos

Lógica Modal de Primeira-Ordem para Raciocinar sobre Jogos; 2007; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Juliana Carpes Imperial

Confiança em Agentes Inteligentes; 2007; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Carlos Bazílio Martins

Análise Formal de Protocolos e Algoritmos Distribuídos: Uma Abordagem Baseada em Linguagem; 2005; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

José Antonio F

de Macedo; Um modelo conceitual para biologia molecular; 2005; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Coorientador: Edward Hermann Haeusler;

Christian Jacques Renteria

Uma Abordagem Geral para Quantificação em Dedução Natural; 2004; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Fernando Náufel do Amaral

Uma Abordagem Categorica baseada em Topoi para Heurísticas; 2004; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Fundação Carlos Chagas Filho de Amparo à Pesquisa do Estado do RJ; Orientador: Edward Hermann Haeusler;

Geiza Maria Hamazaki da Silva

Síntese Construtiva de Programas em Teorias Intuicionistas; 2004; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Marcelo Fagundes Félix

Formal Analysis of Software Mod- els Guided by Architectural Abstractions; 2004; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Cristiano O Braga

Uma abordagem baseada em Lógica de Reescrita para a Semântica Operacional Modular; 2001; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

Isabel Leite Cafezeiro

Compartilhamento e Semântica Denotacional; 2000; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Alex Vasconcelos Garcia

Um Modelo Categórico para Traduções entre Linguagens de Programação; 2000; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Leonardo M Moura

Análise de Programas; 2000; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Coorientador: Edward Hermann Haeusler;

Ana Isabel de Azevedo Spinola

Sistemas Reativos: Uma Abordagem Geométrica; 1999; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Regina Célia Moreth Bragança

Cálculo de Sequentes e Dedução Natural: Relacionamentos e Consequências; 1999; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Eliana Silva Almeida

A Lógica dos Recursos no Formalismo de Redes de Petri; 1998; 0 f; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Edward Hermann Haeusler;

LUCILIA CAMARAO FIGUEIREDO

Lambda/Omega Calculus: Um Lambda Calculus Com Reflexao e Paralelismo; 1997; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Minas Gerais, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Edward Hermann Haeusler;

Marcelo da Silva Corrêa

Categorias e Sequencialidade; 1997; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, ; Orientador: Edward Hermann Haeusler;

Luiz Carlos Castro Guedes

Um Modelo Orientado A Objetos Para A Geracao Automatica de Compiladores; 1995; Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Coorientador: Edward Hermann Haeusler;

Hugo Daniel de Macedo

2015; Conselho Nacional de Desenvolvimento Científico e Tecnológico, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Edward Hermann Haeusler;

Vaston Gonçalves Costa

2009; Pontifícia Universidade Católica do Rio de Janeiro, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Edward Hermann Haeusler;

Produções bibliográficas

PACHECO, CARLA ; PAES, VAGNER ; CARVALHO, MARCELO ; LOPES, FELIPE ; MACHADO, GABRIEL ; GARCIA, ALEX ; NETO, EDMILSON ; SANTOS, JEFFERSON ; HAEUSLER, EDWARD ; MAROTTI, ANA . Enhancing Predictive Maintenance of Power Transformers Through Machine Learning Approaches. LEARNING AND NONLINEAR MODELS , v. 22, p. 19-29, 2024.
Haeusler, Edward Hermann ; RUSSO, CIRO ; SECCO, GISELE . Contemporary Logic in Brazil - Proceedings of the XX Encontro Brasileiro de Lógica. Studia Logica , v. online, p. 1-4, 2024.
Haeusler, Edward Hermann ; RUSSO, CIRO ; SECCO, GISELE . Proceedings of the XX Encontro Brasileiro de Lógica. JOURNAL OF LOGIC AND COMPUTATION , v. online, p. 1-4, 2024.
COSTA, V. G. ; Haeusler, Edward Hermann . Strong Normalization for Np-Systems via Mimp-Graphs. THE IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS , v. 9, p. 135-160, 2022.
Haeusler, Edward Hermann . Exponentially Huge Natural Deduction proofs are Redundant: Preliminary results on M ⊃. THE IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS , v. 9, p. 287-326, 2022.
GIOVANNINI, EDUARDO N. ; Haeusler, Edward H. ; LASSALLE-CASANAVE, ABEL ; VELOSO, PAULO A. S. . DE ZOLT?S POSTULATE: AN ABSTRACT APPROACH. Review of Symbolic Logic , v. 15, p. 197-224, 2022.
GIOVANNINI, EDUARDO N. ; LASSALLE CASANAVE, ABEL ; Haeusler, Edward Hermann . Sobre el Postulado de De Zolt en tres dimensiones. O QUE NOS FAZ PENSAR (PUCRJ) , v. 29, p. 182, 2022.
Lifschitz, Sergio ; Haeusler, Edward H. ; CATANHO, M. ; de Miranda, Antonio Basilio ; de Armas, Elvismary Molina ; HEINE, A. A. P. ; MOREIRA, S. G. ; Tristão, Cristian . Bio-strings: a relational database data-type for dealing with large biosequences. BioTech , v. 11, p. 1-26, 2022.
GORDEEV, LEW ; Haeusler, Edward Hermann . Proof Compression and NP Versus PSPACE II: Addendum. University of Lodz. Department of Logic. Bulletin of the Section of Logic , v. 51, p. 197-205, 2022.
Salgueiro, M. ; DOS SANTOS, VERÔNICA ; REGO, A. L. ; GUIMARAES, D. S. ; SANTOS, J. B. ; Hæusler, Edward Hermann ; Villas, M. ; LIFSCHITZ, S. . Searching for Researchers: an Ontology-based NoSQLDatabase System Approach and Practical Implementation. Journal of Information and Data Management - JIDM , v. 13, p. 538-550, 2022.
WOLTER, U.E. ; MARTINI, A.R. ; HÄUSLER, E.H. . Indexed and fibered structures for partial and total correctness assertions. Mathematical Structures in Computer Science , v. 32, p. 1145-1175, 2022.
VIEIRA, Bruno Lopes ; NALON, C. ; Haeusler, Edward Hermann . Reasoning about Petri Nets: A Calculus Based on Resolution and Dynamic Logic. ACM Transactions on Computational Logic , v. 22, p. 1-22, 2021.
Marins, R. ; OLIVEIRA, R. P. ; Haeusler, Edward H. ; Lifschitz, Sergio ; SCHWABE, D. ; ALMEIDA, A. C. . Outer-Tuning: an Ontology-based Extensible Framework forSupporting Database Automatic Tuning. Journal of Information and Data Management - JIDM , v. 12, p. 156-166, 2021.
WOLTER, U. ; MARTINI, A. ; Haeusler, Edward Hermann . Indexed and Fibred Structures for Hoare Logic. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 348, p. 125-145, 2020.
GORDEEV, LEW ; Haeusler, Edward Hermann . Proof Compression and NP Versus PSPACE II. University of Lodz. Department of Logic. Bulletin of the Section of Logic , v. 49, p. 213-230, 2020.
LIMA, G. ; SANTOS, RODRIGO C. M. ; SANT'ANNA, FRANCISCO ; IERUSALIMSCHY, ROBERTO ; HAEUSLER, EDWARD . A memory-bounded, deterministic and terminating semantics for the synchronous programming language Céu. JOURNAL OF SYSTEMS ARCHITECTURE , p. 239-259, 2019.
Gordeev, L. ; HAEUSLER, E. H. . Proof Compression and NP Versus PSPACE. Studia Logica , v. 107, p. 53-83, 2019.
SLAVIERO, C. ; Haeusler, Edward H. . Computational Thinking Tools: Analyzing concurrency and its representations. SBC JOURNAL ON 3D INTERACTIVE SYSTEMS , v. 9, p. 40-52, 2018.
BENEVIDES, M. R. F. ; LOPES VIEIRA, BRUNO ; Haeusler, Edward Hermann . Towards reasoning about Petri nets: A Propositional Dynamic Logic based approach. THEORETICAL COMPUTER SCIENCE , v. 744, p. 22-36, 2018.
FERNANDES, R. Q. A. ; HAEUSLER, E. H. ; PEREIRA, L. C. P. D. . A Proximity-based Understanding of Conditionals. INTERNATIONAL JOURNAL ON TRANSACTIONS ON LARGE-SCALE DATA- AND KNOWLEDGE-CENTERED SYSTEMS (TLDKS) , v. XXXIV, p. 123, 2017.
Haeusler, Edward Hermann . Finiteness and Computation in Toposes. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE , v. 204, p. 61-77, 2016.
QUISPE-CRUZ, MARCELA ; HAEUSLER, EDWARD ; GORDEEV, LEW . On Strong Normalization in Proof-Graphs for Propositional Logic. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 323, p. 181-196, 2016.
DE BARROS SANTOS, JEFFERSON ; LOPES VIEIRA, BRUNO ; Haeusler, Edward Hermann . A Unified Procedure for Provability and Counter-Model Generation in Minimal Implicational Logic. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 324, p. 165-179, 2016.
MACEDO, HUGO D. ; Haeusler, Edward H. ; GARCIA, ALEX . Defining Effectiveness Using Finite Sets A Study on Computability. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 324, p. 91-106, 2016.
HAEUSLER, E. H. ; Pereira, Luiz Carlos . Two basic results on translations between logics. O QUE NOS FAZ PENSAR (PUCRJ) , v. 25, p. 51-54, 2016.
LUSTOSA, C. ; DOWEK, G. ; Haeusler, Edward Hermann . Yet another bijection between Sequent Calculus and Natural Deduction. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 312, p. 107-124, 2015.
NALON, C. ; VIEIRA, Bruno Lopes ; DOWEK, G. ; Hæusler, Edward Hermann . A calculus for automatic verification of Petri Nets based on Resolution and Dynamic Logics. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 312, p. 125-141, 2015.
Haeusler, Edward Hermann . Propositional Logics Complexity and the Sub-Formula Property. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE , v. 179, p. 1-16, 2015.
Haeusler, Edward Hermann . How Many Times do We Need an Assumption to Prove a Tautology in Minimal Logic? Examples on the Compression Power of Classical Reasoning. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 315, p. 31-46, 2015.
WOLTER, U. ; MARTINI, A. ; Hausler, E. H. . Towards a uniform presentation of logical systems by indexed categories and adjoint situations. Journal of Logic and Computation (Online) , v. 25, p. 57-93, 2015.
CAFEZEIRO, I. L. ; VITERBO, J. ; RADEMAKER, A. ; HAEUSLER, E. H. ; ENDLER, M. . Specifying ubiquitous systems through the Algebra of Contextualized Ontologies. Knowledge Engineering Review (Print) , v. 29, p. 171-185, 2014.
QUISPE-CRUZ, MARCELA ; Haeusler, Edward Hermann ; GORDEEV, LEW . Proof-graphs for Minimal Implicational Logic. Electronic Proceedings in Theoretical Computer Science , v. 144, p. 16-29, 2014.
LOPES, B. ; BENEVIDES, M. ; HAEUSLER, E. H. . Propositional dynamic logic for Petri Nets. Logic Journal of the IGPL (Online) , v. 22, p. 721-736, 2014.
VIEIRA, Bruno Lopes ; Benevides, M. ; HAEUSLER, E. H. . Extending Propositional Dynamic Logic for Petri Nets. Electronic Notes in Theoretical Computer Science , v. 305, p. 67-83, 2014.
ENGLANDER, C. ; PEREIRA, L. C. ; Haeusler, Edward Hermann . Finitely many-valued logics and natural deduction. Logic Journal of the IGPL (Print) , v. advanc, p. 1-22, 2013.
Haeusler, Edward H. . A proof-theoretical discussion on the mechanization of propositional logics. Electronic Proceedings in Theoretical Computer Science , v. 113, p. 7-8, 2013.
HAEUSLER, E. H. ; PEREIRA, L. C. ; VELOSO, P. A. S. . CATEGORIFICAÇÃO, TEORIA DOS CONJUNTOS E FINITUDE. Notae Philosophicae Scientiae Formalis , v. 2, p. 1-22, 2013.
HAEUSLER, E. H. . A celebration of Alan Turing's achievements in the year of his centenary. International Transactions in Operational Research , v. 19, p. 487-491, 2012.
VELOSO, P. A. S. ; PEREIRA, L. C. ; HAEUSLER, E. H. . On what there must be: existence in Logic and some related riddle. Disputatio (Lisboa) , v. 4, p. 889-910, 2012.
Gordeev, L. ; HAEUSLER, E. H. ; PEREIRA, L. C. . Propositional proof compressions and DNF logic. Logic Journal of the IGPL (Print) , v. 19, p. 62-86, 2011.
PAIVA, V. ; RADEMAKER, A. ; HAEUSLER, E. H. . Constructive Description Logics Hybrid-Style. Electronic Notes in Theoretical Computer Science , v. 273, p. 21-31, 2011.
HAEUSLER, E. H. ; PAIVA, V. ; RADEMAKER, A. . Using Intuitionistic Logic as a Basis for Legal Ontologies. Informatica e diritto , v. 1, p. 289-298, 2011.
PEREIRA, L. C. ; Haeusler, Edward H. ; COSTA, V. G. ; SANZ, Wagner . A New Normalization Strategy for the Implicational Fragment of Classical Propositional Logic. Studia Logica , v. 96, p. 95-108, 2010.
RADEMAKER, A. ; HAEUSLER, E. H. . Providing a Proof-Theoretical Basis for Explanation: A Case Study on UML and ALCQI Reasoning. Journal of Universal Computer Science (Online) , v. 16, p. 3016-3042, 2010.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. ; CUKIERMAN, H. L. ; MARQUES, I. C. . Recontando a Computabiliddade. Revista Brasileira de História da Ciência , v. 3, p. 231-251, 2010.
Gordeev, L. ; HAEUSLER, E. H. ; COSTA, V. G. . Proof compressions with circuit-structured substitutions. Journal of Mathematical Sciences (New York) , v. 158, p. 645-658, 2009.
FERNANDES, R. ; HAEUSLER, E. H. . A Topos-Theoretic Approach to Counterfactual Logic. Electronic Notes in Theoretical Computer Science , v. 256, p. 33-47, 2009.
COSTA, V. G. ; SANZ, Wagner ; HAEUSLER, E. H. ; PEREIRA, L. C. . Peirce's rule in a full Natural Deduction system. Electronic Notes in Theoretical Computer Science , v. 256, p. 5-18, 2009.
BRAGA, C. O. ; HAEUSLER, E. H. . Lightweight analysis of access control models with description logic. Innovations in Systems and Software Engineering (Print) , v. 6, p. 115-123, 2009.
VELOSO, P. A. S. ; PEREIRA, L. C. ; HAEUSLER, E. H. . Validades existenciais e enigmas relacionados. Dois Pontos (UFPR) , v. 6, p. 145-163, 2009.
Gordeev, L. ; HAEUSLER, E. H. ; COSTA, V. G. . Proof compressions with circuit-structured substituitions. Zapiski Naucnyh Seminarov Leningradskogo Otdelenia Ordena Lenina Matematiceskogo Instituta im. V.A. Steklova Akademii Nauk SSSR , v. 358, p. 77-99, 2008.
PEREIRA, L. C. ; HAEUSLER, E. H. ; MEDEIROS, M. P. . Alguns resultados sobre fragmentos da lógica proposicional clássica,. O Que nos Faz Pensar (PUCRJ) , v. 23, p. 105-111, 2008.
VASCONCELOS, D. R. ; HAEUSLER, E. H. . Quantifying in extensive games. CLE e-Prints (Online) , v. 8, p. 7, 2008.
RADEMAKER, A. ; PEREIRA, L. C. ; Hæusler, Edward Hermann . On The Proof Theory of ALC. CLE e-Prints , v. 8, p. Article 14, 2008.
COSTA, V. G. ; HAEUSLER, E. H. ; LABER, E. S. ; NOGUEIRA, L. . A note on the size of minimal covers. Information Processing Letters , v. 102, p. 124-126, 2007.
AMARAL, F. N. ; HAEUSLER, E. H. . Using the internal logic of a topos to model search space for problems. Logic Journal of the IGPL , v. 15, p. 457-474, 2007.
MARTINI, A. ; WOLTER, U. ; HAEUSLER, E. H. . Fibred and Indexed Categories for Abstract Model Theory. Logic Journal of the IGPL , v. 15, p. 707-739, 2007.
MARTINS, C. B. ; HAEUSLER, E. H. ; ENDLER, M. . Language-Oriented Formal Analysis: a Case Study on Protocols and Distributed Systems. Electronic Notes in Theoretical Computer Science , v. 184, p. 189-207, 2007.
SILVA, G. M. H. ; HAEUSLER, E. H. ; VELOSO, P. A. S. . Exploring Computational Contents of Intuitionist Proofs. Logic Journal of the IGPL , Oxford - UK, v. 13, n.1, p. 69-93, 2005.
RENTERIA, C. J. ; HAEUSLER, E. H. . A Natural Deduction System for Keisler Logic. Electronic Notes in Theoretical Computer Science , v. 123, p. 229-240, 2005.
MARTINS, C. B. ; HAEUSLER, E. H. ; ENDLER, M. . Binding Network Topologies to Specifications via Pronouns. Annals of Mathematics, Computing & Teleinformatics , v. 1, p. 1-7, 2005.
RENTERIA, C. J. ; HAEUSLER, E. H. ; VELOSO, P. A. S. . NUL: A Natural Deduction for Ultrafilter Logic. Bulletin of the Section of Logic , Lodz, v. 32, n.4, p. 191-200, 2003.
RENTERIA, C. J. ; HAEUSLER, E. H. . Natural Deduction for CTL. Bulletin of the Section of Logic , Polonia, v. 31, n.4, p. 231-240, 2002.
GARCIA, Alex V. ; HAEUSLER, E. H. . Code Migration and Program Maintainability - A Categorical Perspective. Information Processing Letters , Holanda, v. 79, n.5, p. 249-254, 2001.
GARCIA, Alex V. ; HAEUSLER, E. H. . A Categorical Model for Programming Languages Translation. Electronic Notes in Theoretical Computer Science , Nova Iorque, v. XX, p. 1-15, 2000.
De MOURA, L. ; LUCENA, C. J. P. ; HAEUSLER, E. H. . Analysis of Parallel Programs. Electronic Notes in Theoretical Computer Science , Nova Iorque, v. XX, p. 1-15, 2000.
AMARAL, F. N. ; HAEUSLER, E. H. . A Logic-Based Approach for Real-Time Object-Oriented Software Development. Revista de Informática Teórica e Aplicada , Porto Alegre - RS, v. 7, n.1, p. 69-88, 2000.
AMARAL, F. N. ; HAEUSLER, E. H. . Completeness of an Action Logic for Timed Transition Systems. Bulletin of the Section of Logic , Polonia, v. 29, n.4, p. 151-160, 2000.
PEREIRA, L. C. ; HAEUSLER, E. H. . An Infinitary Extension of MALL-. Bulletin of the Section of Logic , Lodz, v. 28, n.4, p. 225-233, 1999.
ALMEIDA, E. S. ; HAEUSLER, E. H. . Proving Properties in Ordinary Petri Nets using LoRes logical language. Petri Nets Newsletter, Karlsruhe, v. 57, p. 23-36, 1999.
HAEUSLER, E. H. ; PEREIRA, L. C. . The Rules-as-Types Interpretation of Schroeder-Heister's Extension of Natural Deduction. Manuscrito (UNICAMP) , Campinas, v. XXII, n.2, p. 149-164, 1999.
VELOSO, P. A. S. ; HAEUSLER, E. H. . Extracting Solutions from Constructive Proofs: Towards a Programming Methodology. Brazilian Eletronic Journal Of Mathematics Of Computation, Pelotas, v. 0, n.0, p. 1-31, 1999.
SPINOLA, A. I. A. ; HAEUSLER, E. H. . A Semi-Sheaf Theoretical Approach to Reactive Systems. Brazilian Eletronic Journal Of Mathematics Of Computation, Pelotas, v. 0, n.0, p. 1-17, 1999.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. . Programming language syntax: expressing sharing. Monografias em Ciência da Computação , v. 1999, p. 9, 1999.
HAEUSLER, E. H. ; PEREIRA, L. C. . Gentzen'S Second Consistency Proof And Strong Cut-Elimination. Logique et Analyse , Bélgica, v. 153, p. 95-111, 1998.
CORRÊA, M. S. ; Haeusler, Edward Hermann . A Concrete Categorical Model for the Lambek Syntactic Calculus. Mathematical Logic Quarterly , GREISWALD, ALEMANHA, v. 43, n.2, p. 49-59, 1997.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. ; HAEBERER, A. . From diagram to code via attribute grammar. Monografias em Ciência da Computação , v. 1997, p. 03, 1997.
HAEUSLER, E. H. . Generating Programs From Problems: Interaction Between Problem Theory And Type Theory. Investigación Operativa , Chile, v. 5, n.2-3, p. 153-168, 1996.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. ; LUCENA, C. J. P. . Paradigmas de linguagens de programação: uma abordagem geométrica. Monografias em Ciência da Computação , v. 1996, p. 21, 1996.
HAEUSLER, E. H. ; PEREIRA, L. C. . A formalization of Sambins's normalization for GL. Mathematical Logic Quarterly , GREISWALD, ALEMANHA, v. 39, n.1, p. 133-142, 1993.
HAEUSLER, E. H. ; BITTEL, O. . On The Relationship Between Well-Orderings In Intuitionistic Type Theory And Data-Types Inductively Defined. O Que nos Faz Pensar , RIO DE JANEIRO, v. MAR/91, p. 61-79, 1991.
HAEUSLER, E. H. . Automatic Theorem Proving: An Attempt To Improve The Readability Of Proofs Generated By Resolution.. Contemporary Mathematics. American Mathematical Society , RHODE ISLAND, NY, v. 69, p. 179-188, 1988.
GIOVANNINI, E. ; Hæusler, Edward Hermann ; Lassale Casanave, A. . The Theory of Plane Area at the Crossroads. 1. ed. Springer-Verlag, 2024. v. 1. 146p .
HAEUSLER, E. H. ; PEREIRA, L. C. P. D. (Org.) ; VIANA, J. P. (Org.) . A Question is More Illuminating than an Answer. A Festschrift for Paulo A. S. Veloso. 1. ed. Londres: College Publications, 2021.
Haeusler, Edward Hermann ; SANZ, Wagner ; VIEIRA, Bruno Lopes . Why is this a Proof ? Festschrift for Luiz Carlos Pereira. 1. ed. College Publications, 2015.
PEREIRA, L. C. ; HAEUSLER, E. H. ; PAIVA, V. . A Celebration of Dag Prawitz's Work. 1. ed. Springer-Verlag, 2013.
AYALA-RINCÓN, M. (Org.) ; HAEUSLER, E. H. (Org.) . V.1, n. 18 of Logic Journal of IGPL. Oxford: Oxford University Press, 2009.
AYALA-RINCÓN, M. (Org.) ; HAEUSLER, E. H. (Org.) . Volume 205 ENTCS . Post-Proceedings of LFSA 2007. 205. ed. Amsterdam: Elsevier, 2008. 144p .
BALDWIN, J. T. (Org.) ; QUEIROZ, R. (Org.) ; HAEUSLER, E. H. (Org.) . 8th Workshop on Logic, Language, Informations and Computation. Rio de Janeiro: Sociedade Brasileira de Matemática (SBM), 2003. 183p .
QUEIROZ, R. (Org.) ; PEREIRA, L. C. (Org.) ; HAEUSLER, E. H. (Org.) . Proceedings of the WOLLIC'2002. 1. ed. NY: Elsevier Science, 2002.
HAEUSLER, E. H. ; FIGUEIREDO, C. C. (Org.) ; GARCIA, Alex V. (Org.) ; CERQUEIRA, R. (Org.) . Anais do Simpósio Brasileiro de Linguagens de Programação. Rio de Janeiro: PUC-Rio , SBC, 2002.
MUSICANTE, M. A. (Org.) ; HAEUSLER, E. H. (Org.) . Anais do V SImpósio Brasileiro de Linguagens de Programação. Paraná: Universidade Federal do Paraná - SBC, 2001. v. 250. 275p .
MELO, A. C. V. (Org.) ; HAEUSLER, E. H. (Org.) . Proceedings of the IV WMF. Rio de Janeiro: UFRJ - SBC -IME, 2001. v. 250. 120p .
MENEZES, P. B. ; HAEUSLER, E. H. . Teoria das Categorias e Ciência da Computação. 1. ed. Porto Alegra- RS: Sagra/Luzzato/UFRGS, 2001. v. 1000. 350p .
HAEUSLER, E. H. ; PEREIRA, L. C. . PRATICA:Proofs, Types and Categories. 1. ed. Rio de Janeiro: Independente, 1999. v. 1. 219p .
PEREIRA, L. C. (Org.) ; HAEUSLER, E. H. (Org.) . Pre-Proceedings of The XII Brazilian Logic Meeting. Rio de Janeiro: Sociedade Brasileira de Lógica, 1999. v. 1. 149p .
Pereira, Luiz Carlos ; Haeusler, Edward Hermann ; Nascimento, Victor . Disjunctive Syllogism without Ex falso. In: Piecha, T.; Wehmeier, K.F.. (Org.). Outstanding Contributions to Logic. 1ed.Cham: Springer Nature Switzerland, 2024, v. 29, p. 193-209.
ALKMIN, B. ; Haeusler, Edward H. ; SCHWABE, D. . A Case Study Integrating Knowledge Graphs and Intuitionistic Logic. In: Víctor Rodríguez-Doncel; Monica Palmirani ; Michał Araszkiewicz ; Pompeu Casanovas ;Ugo Pagallo ; Giovanni Sartor. (Org.). AI Approaches to the Complexity of Legal Systems XI-XII (LNAI). 1ed.Zurique: Springer-Nature, 2021, v. 13048, p. 106-124.
Hæusler, Edward Hermann . Uma nota sobre resultados de speed-up em complexidade e lógica. In: Gisele Dalva Secco; Frank Thomas Sautter;Oscar MIguel Esquisavel; Wagner Sanz. (Org.). De Mathematicae atque Philosophicae Elegantia. 1ed.Londres: College Publications, 2021, v. 18, p. 85-100.
Busson, Antonio José G. ; Guedes, Álan Livio V. ; COLCHER, SÉRGIO ; Milidiú, Ruy Luiz ; Haeusler, Edward Hermann . Embedding Deep Learning Models into Hypermedia Applications. In: Roesler, Valter and Barrère, Eduardo and Willrich, Roberto. (Org.). Special Topics in Multimedia, IoT and Web Technologies. 1ed.Cham: Springer International Publishing, 2020, v. , p. 91-111.
de Armas, Elvismary Molina ; Ferreira, Paulo Cavalcanti Gomes ; Haeusler, Edward Hermann ; de Holanda, Maristela Terto ; Lifschitz, Sérgio . K-mer Mapping and RDBMS Indexes. Lecture Notes in Computer Science. 1ed.: Springer International Publishing, 2020, v. , p. 70-82.
Tristão, Cristian ; de Miranda, Antonio Basilio ; Haeusler, Edward Hermann ; Lifschitz, Sergio . Relational Text-Type for Biological Sequences. Lecture Notes in Computer Science. 1ed.: Springer International Publishing, 2020, v. , p. 102-112.
Entenza, Julio Omar Prieto ; Haeusler, Edward Hermann ; Lifschitz, Sérgio . Efficient Out-of-Core Contig Generation. Lecture Notes in Computer Science. 1ed.: Springer International Publishing, 2020, v. , p. 25-37.
Haeusler, Edward H. ; Rademaker, Alexandre . On how kelsenian jurisprudence and intuitionistic logic help to avoid contrary-to-duty paradoxes in legal ontologies. In: Edgar Almeida; Alexandre Costa-Leite; Rodrigo Freire. (Org.). Seminário Lógica no Avião. 1ed.Brasilia: Lógica no Avião, 2019, v. 1, p. 44-59.
MACEDO, HUGO D. ; Haeusler, Edward Hermann . Yoneda?s Embedding and Post-Completeness. In: Jean-Yves Beziau; Francicleber Ferreira; Ana Teresa Martins; Marcelo Pequeno. (Org.). Yoneda?s Embedding and Post-Completeness. 1ed.Londres: College Publications, 2018, v. 38, p. 1-12.
de Araujo Fernandes, Ricardo Queiroz ; Haeusler, Edward Hermann ; Pereira, Luiz Carlos Pinheiro Dias . A Proximity-Based Understanding of Conditionals. Lecture Notes in Computer Science. 1ed.Berlin: Springer Berlin Heidelberg, 2017, v. , p. 123-152.
Pereira, Luiz Carlos ; Haeusler, Edward Hermann . On Constructive Fragments of Classical Logic. In: Heinrich Wansing. (Org.). Outstanding Contributions to Logic. 1ed.: Springer International Publishing, 2015, v. , p. 281-292.
HAEUSLER, E. H. ; PEREIRA, L. C. . Fibonacci estimation for the height of Schutte-like cut-free proofs. In: Jean-Yves Beziau and Marcelo Esteban Coniglio. (Org.). Logic without Frontiers:Festschrift for Walter Alexandre Carnielli on the occasion of his 60th Birthday. London: College Publications, 2011, v. 17, p. 97-104.
RADEMAKER, A. ; HAEUSLER, E. H. . Is it important to explain a theorem ? A case study on UML and ALCQI. In: C.A. Heuser and G. Pernul. (Org.). ER-2009, Proceedings, LNCS. 1ed.Berlim: Springer-Verlag, 2009, v. 5833, p. 34-44.
VASCONCELOS, D. R. ; HAEUSLER, E. H. . Quantifying in Extensive Games. In: Walter Carnielli; Marcelo Coniglio ; Itala D'Otaviano. (Org.). The Many Sides of Logic. London: College Publications, 2009, v. 21, p. 321-336.
RADEMAKER, A. ; Hæusler, Edward Hermann ; PEREIRA, L. C. . On the Proof Theory of ALC. In: Walter Carnielli; Marcelo Coniglio; Itala D'Ottaviano. (Org.). The Many Sides of Logic. London: College Pulications, 2009, v. 21, p. 273-285.
CAFEZEIRO, I. L. ; Hæusler, Edward Hermann . Algebraic Framework for Reverse Engineering on Specifications. In: Minoro Abe, J.. (Org.). Frontiers in Artificial Intelligence and Applications. 1ed.Amsterdam: IOS, 2009, v. 186, p. 1-12.
HAEUSLER, E. H. ; MARTINI, A. ; WOLTER, U. . Some Models of Heterogeneous and Distributed Specifications based on Universal Constructions. In: J. Y. Beziau and A. Costa-leite. (Org.). Perspectives on Universal Logic. Monza: Polimétrica, 2007, v. , p. 297-318.
ABOIM, D. S. ; SOUZA, C. S. ; HAEUSLER, E. H. . Structured Argument Generation in a Logic Based KB-System. In: Lawrence S. Moss; Jonathan Ginzburg; Maarten de Rijke. (Org.). Logic Language and Computation. 1ed.Stanford, California: CSLI Publications, 1999, v. 2, p. 237-265.
FIGUEIREDO, L. C. ; HAEUSLER, E. H. . Another Approach To Abramsky'S Proofs-As-Processes For Multiplicative Linear Logic. In: Walter A. Carnielli; Luiz Carlos P.D. Pereira. (Org.). LOGIC, SETS AND INFORMATION. 1ed.CAMPINAS: ED. UNICAMP, 1995, v. 14, p. 107-135.
CRAIZER, LUIS ; Hermann, Edward ; SILVA, MOACYR . Deep Reinforcement Learning for Auctions: Evaluating Bidding Strategies Effectiveness and Convergence. In: 17th International Conference on Agents and Artificial Intelligence, 2025, Porto. Proceedings of the 17th International Conference on Agents and Artificial Intelligence, 2025. p. 367-376.
CRAIZER, LUIS ; Hermann, Edward ; SILVA, MOACYR . Leveraging Transfer Learning to Improve Convergence in All-Pay Auctions. In: 27th International Conference on Enterprise Information Systems, 2025, Porto. Proceedings of the 27th International Conference on Enterprise Information Systems. Setúbal: SCITEPRESS - Science and Technology Publications, 2025. v. 1. p. 534-543.
COSTA NETO, L. H. ; LIFSCHITZ, S. ; Baião, F. ; CATANHO, M. ; MIRANDA, ANTONIO B. ; Hæusler, Edward Hermann . On the Expressiveness of Petri Nets for Modeling Biological Processes: The Case for mRNA Translation and Protein Synthesis. In: Conpectual Modeling in Life Sciences, 2024, Pittsburgh. Proceedings of the CMLS 2024, 2024. v. 14932. p. 137-147.
GUATEQUE, M. L. ; de Miranda, Antonio Basilio ; CATANHO, M. ; HAEUSLER, E. H. ; LIFSCHITZ, S. . An Approach for Modeling and Analysis of Insulin Biosynthesis using Petri Nets. In: IEEE Conference on Computational Intelligence in Bioinformatics and Computational Biology (CIBCB), 2024, Natal. IEEE Conference on Computational Intelligence in Bioinformatics and Computational Biology, CIBCB 2024. Los Alamitos: IEEE, 2024. p. 1-8.
PINTO, FERNANDO ANTONIO D. G. ; SANTOS, J. B. ; LIFSCHITZ, S. ; Hausler, E. H. . A Two-tiered Approach for Knowledge Reasoning. In: SBBD 2024, 2024, Florianópolis. Proceedings of the 39th Brazilian Symposium on Data Bases. Porto Alegre: SBC, 2024. p. 652-658.
SARAIVA, L. ; Haeusler, Edward H. ; COSTA, V. G. . Quantum Algorithm for Multiplicative Linear Logic. In: Workshop Brasileiro de Lógica, 2023, João Pessoa. Anais do IV Workshop Brasileiro de Lógica. Porto Alegre: Sociedade Brasileira de Computação, 2023. p. 33-40.
CALLOU, R. ; SANTOS, J. B. ; Haeusler, Edward H. . On the Coverage Property of a Derivation Compression Algorithm. In: Workshop Brasileiro de Lógica, 2023, João Pessoa. Anais do IV Workshop Brasileiro de Lógica. Porto Alegre: Sociedade Brasileira de Computação, 2023. p. 1-8.
Haeusler, Edward H. ; CUCONATO, B. ; GLATZ, L. A. ; GUATEQUE, M. L. ; VIEIRA, D. M. ; ARMAS, E. M. ; Baião, F. ; CATANHO, M. ; de Miranda, Antonio Basilio ; Lifschitz, Sergio . Intentional Semantics for Molecular Biology. In: Brazilian Symposium on Bioinformatics, 2023, Curitiba. Proceedings of the Brazilian Symposium on Bioinformatics. Berlin: Springer-Verlag, 2023. p. 1-16.
PINTO, FERNANDO ANTONIO D. G. ; SANTOS, J. B. ; LIFSCHITZ, S. ; Haeusler, Edward Hermann . A benchmarking for public information by Machine Learning and Regular Language. In: WORKSHOP DE COMPUTAÇÃO APLICADA EM GOVERNO ELETRÔNICO, 2023, João Pessoa. 2023: ANAIS DO XI WORKSHOP DE COMPUTAÇÃO APLICADA EM GOVERNO ELETRÔNICO. Porto Alegre: Sociedade Brasileira de Computação, 2023. p. 1-12.
VIEIRA, DIOGO MUNARO ; de Armas, Elvismary Molina ; JARAMILLO, MARIA L. G. ; CATANHO, MARCOS ; MIRANDA, ANTONIO B. ; Haeusler, Edward Hermann ; Lifschitz, Sérgio . A New Data Modeling Approach for Alignment-free Biological Applications. In: Simpósio Brasileiro de Banco de Dados, 2023, Brasil. Anais do XXXVIII Simpósio Brasileiro de Banco de Dados (SBBD 2023). p. 1-13.
DOS SANTOS, VERÔNICA ; Haeusler, Edward Hermann ; SCHWABE, D. ; LIFSCHITZ, S. . Context-Aware Knowledge Graphs Exploratory Search. In: Simpósio Brasileiro de Banco de Dados, 2023, Belo Horizonte. Anais do XXXVIII Simpósio Brasileiro de Banco de Dados. Porto Alegre: Sociedade Brasileira de Computação, 2023. p. 360-365.
PACHECO, C. ; PAES, V. ; MACHADO, G. ; CARVALHO, M. ; LOPES, F. ; GARCIA, Alex V. ; Edmilson Siqueira Varejão Neto ; SANTOS, J. B. ; HAEUSLER, E. H. ; MAROTTI, A. C. F. . On the use of Machine Learning for predictive maintenance of power transformers. In: Brazilian Conference on Computatioal Intelligence, 2023, Salvador. Proceedings of the XVI Brazilian Conference on Computational Intelligence. Salvador: Sociedade Brasileira de Inteligência Computacional, 2023. p. 1-8.
PINTO, FERNANDO ANTONIO D. G. ; LIFSCHITZ, S. ; Haeusler, Edward H. . A knowledge base of public acts based on the grammar of the Official Gazette. In: The International IEEE Conference on Digital Government Technology and Innovation (DGTi-Con 2022), 2022, Bang Kok. Proceedings of the International Conference on Digital Government Technology and Innovation (DGTi-Con 2022). IEEE-publisher: IEEE, 2022. p. 24-29.
CARVALHO, M. ; MAROTTI, A. ; GARCIA, Alex V. ; RODRIGUES, A. C. ; BRITO, L. M. ; FERREIRA, C. C. C. P. ; MACHADO, G. R. ; VAREJAO, E. ; SCHNEIDER, P. H. ; SANTOS, J. B. ; BARG, M. R. W. ; GUTTLER, C. ; Haeusler, Edward Hermann . EnSights: Monitoramento Inteligente de Ativos de Transmissão.. In: Seminário Nacional de Produção e Transmissão de Energia Elétrica (SNPTEE2022), 2022, Rio de Janeiro. Anais do XXVI Seminário Nacional de Produção e Transmissão de Energia Elétrica (SNPTEE2022), 2022. v. 3. p. 50.
PINTO, FERNANDO ANTONIO D. G. ; Lifschitz, Sérgio ; Haeusler, Edward Hermann . A Graph Knowledge-base for Auditing Human Resources Public Management. In: Workshop de Computação Aplicada em Governo Eletrônico, 2022, Brasil. Anais do X Workshop de Computação Aplicada em Governo Eletrônico (WCGE 2022), 2020. p. 61-72.
ALKMIN, B. ; Haeusler, Edward Hermann ; NALON, C. . A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals. In: Description Logic 2022, 2022, Haifa - Israel. Proceedings of the DL2022. Aachen- Alemanha: CEURS, 2022. v. XXX.
CALLOU, R. ; SANTOS, J. B. ; Haeusler, Edward H. . Towards a Proof in Lean about the Horizontal Compression of Dag-Like Derivations in Minimal Purely Implicational Logic. In: The Seventeenth International Workshop on Logical and Semantic Frameworks, with Applications, 2022, Belo Horizonte e Online. The Seventeenth International Workshop on Logical and Semantic Frameworks, with Applications. Belo Horizonte: UFMG, 2022. p. 8-23.
SALGUEIRO, MARIANA D. A. ; Lifschitz, Sérgio ; Haeusler, Edward Hermann ; DOS SANTOS, VERÔNICA ; HEINE, ALEXANDRE A. P. . A Study of Database Models for Social Network Analysis. In: Simpósio Brasileiro de Banco de Dados, 2022, Brasil. Anais do XXXVII Simpósio Brasileiro de Banco de Dados (SBBD 2022). Porto Alegre: Sociedade Brasileira de Computação - SBC, 2022. p. 397-402.
GARCIA, Alex V. ; Gabriel Resende Machado ; CASTRO, C. C. ; Haeusler, Edward H. ; SANTOS, J. B. ; Edmilson Siqueira Varejão Neto ; Schenider Pedro ; BARBOSA, A. S. ; MAGALHAES, M. ; CARVALHO, M. ; MAROTTI, A. C. F. . ENSIGHTS: Intelligent Monitoring of Electric Power Transmission Assets. In: European Conference on the Impact of AI and Robotics (ECIAIR 2022), 2022, London. European Conference on the Impact of AI and Robotics : Conference Proceedings. London: Academic Conferences International Limited, 2022. v. 4. p. 36-44.
PINTO, FERNANDO ANTONIO D. G. ; Haeusler, Edward Hermann ; Lifschitz, Sérgio . Transparência pública automatizada a partir da gramática do diário oficial. In: Workshop de Computação Aplicada em Governo Eletrônico, 2021, Brasil. Anais do IX Workshop de Computação Aplicada em Governo Eletrônico (WCGE 2021). Porto Alegre: Sociedade Brasileira da Computação, 2021. p. 59-70.
ALKMIM, B. P. ; HAEUSLER, E. H. ; SCHWABE, D. . Reasoning over Knowledge Graphs in an Intuitionistic Description Logic. In: XAILA at Jurix EXplainable and Responsible AI in Law, 2021, Prague. Proceedings of the 3rd EXplainable AI in Law Workshop (XAILA 2020). Sydney: CEURS, 2020. v. 2891. p. 1-12.
Perciliano, L. ; Santos, V. ; Baião, F. ; HAEUSLER, E. H. ; Lifschitz, Sergio ; ALMEIDA, A. C. . Inferencing Relational Database Tuning Actions with OnDBTuning Ontology. In: Simpósio Brasileiro de Banco de Dados, 2021, Rio de Janeiro. Proceedings of the SBBD 2021, 2021.
Salgueiro, M. ; LIFSCHITZ, S. ; Villas, M. ; HAEUSLER, E. H. ; SANTOS, J. . Sistemas de Recuperação de Informações Aplicados à Produções Acadêmicas. In: WTAG - SBBD, 2021, Rio de Janeiro. Anais do WTAG, 2021.
Salgueiro, M. ; Santos, V. ; REGO, A. L. ; GUIMARAES, D. S. ; HAEUSLER, E. H. ; SANTOS, J. ; Villas, M. ; LIFSCHITZ, S. . Quem@ PUC-A tool to find researchers at PUC-Rio. In: Simpósio Brasileiro de Bancos de Dados, 2021, Rio de Janeiro. Anais Estendidos do XXXVI Simpósio Brasileiro de Bancos de Dados. Porto Alegre: SBC, 2021. p. 93-98.
SLAVIEIRO, C. ; Haeusler, Edward Hermann . A-Games: using game-like representation for representing finite automata. In: Workshop Escola de Informática Teórica, 2021, Bagé. Anais do WEIT2021. Porto Alegre: SBC, 2021. p. 25-32.
SILVA, G. F. ; Haeusler, Edward Hermann ; NALON, C. . Description of Command and Control Networks in Coq. In: Workshop Escola de Informática Teórica, 2021, Bagé. Anais do WEIT2021. Porto Alegre: SBC, 2021. p. 60-67.
SARAIVA, L. ; Hæusler, Edward Hermann ; COSTA, V. G. ; KALINOWSKI, M. . Non-functional requirements of quantum programs. In: 2nd Quantum Software Engineering and Technology Workshop,, 2021, Virtual Conference. roceedings of the 2nd Quantum Software Engineering and Technology Workshop. Madri: CEURS, 2021. v. 3008. p. 89-100.
SILVA, G. F. ; Hæusler, Edward Hermann ; VIEIRA, Bruno Lopes . Formalization of Cryptography Algorithms in the Lean Theorem Prover. In: Logic and Semantic Frameworks with Applications, 2020, Salvador. Proceedings of the LSFA 2020. Salvador: SBC/UFBA, 2020. p. 122-127.
Lifschitz, Sérgio ; Haeusler, Edward Hermann ; TRISTAN, C. . Relational Text-type for Biological Sequences. In: Conceptual Modelling For Life Sciences, 2020, Vienna. Proceedings of the CMLS. Vienna, 2020.
ENTENZA, J. O. ; Haeusler, Edward Hermann ; Lifschitz, Sérgio . Efficient Out-of-core Contig Generation. In: Simpósio Brasileiro de Bioinformática, 2020, São Paulo. Lecture Notes in Bioinformatics. Berlin: Springer-Verlag, 2020.
REIS, RUHAN DOS ; ENDLER, MARKUS ; DE ALMEIDA, VITOR PINHEIRO ; Haeusler, Edward Hermann . A Soft Real-Time Stream Reasoning Service for the Internet of Things. In: 2019 IEEE 13th International Conference on Semantic Computing (ICSC), 2019, Newport Beach. 2019 IEEE 13th International Conference on Semantic Computing (ICSC). Los Alamitos: IEEE, 2019. p. 166.
SANTOS, RODRIGO C. M. ; LIMA, GUILHERME F. ; SANT'ANNA, FRANCISCO ; IERUSALIMSCHY, ROBERTO ; Haeusler, Edward H. . A memory-bounded, deterministic and terminating semantics for the synchronous programming language Céu. In: the 19th ACM SIGPLAN/SIGBED International Conference, 2018, Philadelphia. Proceedings of the 19th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems - LCTES 2018. Philadelphia: ACM, 2018. p. 1.
ALMEIDA, A. C. ; HAEUSLER, E. H. ; LIFSCHITZ, S. ; OLIVEIRA, R. P. ; SCHWABE, D. . Outer-Tuning: sintonia Fina Autom{\'{a}}tica Baseada em Ontologia. In: SBBD, 2018, Rio de Janeiro. SBBD. Companion. Rio de janeiro: Sociedade Brasileira de Computação, 2018.
ALKMIM, B. P. ; RADEMAKER, A. ; Haeusler, Edward Hermann . Utilizing iALC to Formalize the BrazilianOAB Exam. In: EXplainable AI in Law, XAILA@JURIX, 2018, Groningen. Proceedings of the EXplainable AI in Law Workshop. Groningen: CEUR Worshop Proceedings, 2018. v. 2381. p. 42-50.
ENDLER, MARKUS ; BRIOT, JEAN-PIERRE ; SILVA, FRANCISCO SILVA E ; ALMEIDA, VITOR P. DE ; Haeusler, Edward H. . An Approach for Real-Time Stream Reasoning for the Internet of Things. In: 2017 IEEE 11th International Conference on Semantic Computing (ICSC), 2017, San Diego. 2017 IEEE 11th International Conference on Semantic Computing (ICSC), 2017. p. 348-353.
SANTOS, J. ; VIEIRA, Bruno Lopes ; Haeusler, Edward Hermann . Counter-model Generation from Failed Proof Searches in Propositional Minimal Implicational Logic. In: LSFA, 2017, Brasilia. Proceedings of 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017). Brasilia: UnB, 2017.
LIMA, GUILHERME F. ; AZEVEDO, ROBERTO GERSON DE ALBUQUERQUE ; COLCHER, SÉRGIO ; Haeusler, Edward Hermann . Converting NCL Documents to Smix and Fixing Their Semantics and Interpretation in the Process. In: 23rd Brazillian Symposium on Multimedia and the Web, 2017, Gramado. Proceedings of the 23rd Brazillian Symposium on Multimedia and the Web - WebMedia '17, 2017. p. 109.
Delfino, P. ; Cucolato, B. ; HAEUSLER, E. H. ; RADEMAKER, A. . Passing the Brazilian OAB Exam: Data Preparation and Some Experiments. In: Legal Knowledge and Information Systems - JURIX 2017: The Thirtieth Annual Conference, 2017, Luxembourg. Frontiers in Artificial Intelligence and Applications: Legal Knowledge and information systems. Amsterdam: IOS, 2017. v. 302. p. 89-94.
ENDLER, MARKUS ; BRIOT, JEAN-PIERRE ; SILVA E SILVA, FRANCISCO ; DE ALMEIDA, VITOR P. ; Haeusler, Edward H. . Towards stream-based reasoning and machine learning for IoT applications. In: 2017 Intelligent Systems Conference (IntelliSys), 2017, United Kingdom. 2017 Intelligent Systems Conference (IntelliSys). Los Alamitos: IEEE, 2017. p. 202.
Gordeev, L. ; HAEUSLER, E. H. . Compression of proofs and NP vs PSPACE. In: GETFUN4.0/IJCAR2016, 2016, Coimbra. Pre-Proceedings of GETFUN4.0. Coimbra: University of Coimbra, 2016.
BENEVIDES, M. R. F. ; VIEIRA, Bruno Lopes ; Haeusler, Edward H. . Propositional Dynamic Logic for Petri Nets with Iteration. In: ICTAC - International Colloquium on Theoretical Aspects of Computing, 2016, Taipei. Proceedings of ICTAC, LNCS. Berlin: Springer-Verlag, 2016. v. 9965. p. 441-456.
FERNANDES, R. ; PEREIRA, L. C. ; Haeusler, Edward Hermann . PUC-Logic. In: COIN/DEXA International Conference, 2016, Porto. Proceedings of the Consistency and Inconsistency Workshop of DEXA conference. Los Alamitos: IEEE, 2016. p. 102-105.
Haeusler, Edward H. ; RADEMAKER, A. . How Kelsenian Jurisprudence and Intuitionistic Logic help to avoid Contrary-to-Duty paradoxes in Legal Ontologies. In: 3rd Workshop on Logical Reasoning and computation, 2016, Toulouse. Proceeding of the 3rd workshop on Logical Reasoning and computation. Toulouse: Univ. Toulouse., 2015. p. 55-68.
BRAGA, C. O. ; Haeusler, Edward Hermann . Notes on Topoi and Refinement. In: Escola de Informática Teórica e Métodos Formais, 2016, Natal. Anais do ETMF 2016, 2016. p. 21-32.
LIMA, G. ; BRAGA, C. O. ; Haeusler, Edward Hermann . The Smix synchronous multimedia language: Operational semantics and coroutine implementation. In: Escola de Informática Teórica e Métodos Formais, 2016, Natal. Anais do ETMF 2016, 2016. p. 145-154.
LIFSCHITZ, S. ; ARMAS, E. ; Haeusler, Edward Hermann ; HOLANDA, M. T. ; P.C.G., F. ; Silva, W.M.C. . An index-based RDBMS approach for K-mer Mapping and memoryaware fragment assembly. In: The 3rd International Workshop on High Performance Computing on Bioinformatics (HPCB 2016), 2016, Shenzen. Proceedings of the 3rd International Workshop on High Performance Computing on Bioinformatics (HPCB 2016). IEEE BIBM: IEEE, 2016. p. 882-889.
OLIVEIRA, R. D. ; LIFSCHITZ, S. ; ALMEIDA, A. C. ; HAEUSLER, E. H. . Projeto e implementação do framework Outer-tuning: auto sintonia e ontologia para bancos de dados relacionais.. In: Simpósio Brasileiro de Sistemas de Informação, 2015, Goiânia. Proceeding of the XI Brazilian Symposium on Information Systems. Goiânia: SBC-UFG, 2015. v. 1. p. 171-178.
VIEIRA, B. L. ; BENEVIDES, M. ; Haeusler, Edward H. . Reasoning about Multi-Agent Systems Using Stochastic Petri Nets. In: 13th Conference on Practical Applications of Agents, Multi-Agent Systems and Sustainability, 2015, Salamanca. Trends in Practical Applications of Agents, Multi-Agent Systems and Sustainability. London: Springer-Verlad, 2015. v. 372. p. 75-86.
CRUZ, M. Q. ; HAEUSLER, E. H. ; Gordeev, L. . On Strong Normalization in Proof-graphs for Propositional Logic. In: Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015, Natal. Proceedingos of the Tenth Workshop on Logical and Semantic Frameworks, with Applications. Natal: UFRN, 2015. p. 85-101.
MACEDO, H. ; Haeusler, Edward Hermann . Defining Effectiveness Using Finite Sets ? A Study on Computability. In: 3ro Workshop-Escola de Informática Teórica (WEIT2015), 2015, Porto Alegre. Proceedings of WEIT2015. Porto Alegre: UFRGS, 2015.
SANTOS, J. ; VIEIRA, Bruno Lopes ; Haeusler, Edward Hermann . Towards a Unified Procedure for Provability and Counter-Model Generation in Minimal Implicational Logic. In: 3ro Workshop-Escola de Informática Teórica (WEIT2015), 2015, Porto Alegre. Proceedings of WEIT2015. Porto Alegre: UFRGS, 2015.
Haeusler, Edward Hermann . Finiteness and Computation in Toposes. In: DCM 2015 at ICTAC, 2015, Cali. Pre-Proceedings of DCM 2015. Cali: Universidad Javeriana, 2015. p. 27-38.
PEREIRA, L. C. ; Haeusler, Edward H. . The Russell-Prawitz translation and schematic rules: a view from proof-theory. In: General Proof Theory. Celebrating 50 Years of Dag Prawitz's 'Natural Deduction', 2015, Tuebingen. Proceedings of the Conference held in Tübingen, 27-29 November 2015. Tuebingen: Mathematisch-Naturwissenschaftliche Fakultät Tuebingen, 2016. p. 29-54.
HAEUSLER, E. H. ; AYALA-RINCÓN, M. . On the Computability of Relations on λ-Terms and Rice?s Theorem - The Case of the Expansion Problem for Explicit Substitutions. In: LATIN2012, 2014, Montevideo. LATIN2014: Theoretical Informatics, Lecture Notes on Computer Science. Berlin-Heidelberg: Springer-Verlag, 2014. v. 8392. p. 202-213.
PEREIRA, L. C. ; HAEUSLER, E. H. . Cut-elimination and consistency: variations on a Gentzen-Prawitz theme. In: Gentzen's and Jaśkowski's heritage; 80 years of Natural Deduction and Sequent Calculi, 2014, Lodz. Proceedings of Trends in Logic XIII. Lodz: Lodz Universty Press, 2014. p. 165-179.
HAEUSLER, E. H. . Propositional Logics Complexity and the sub-formula Property. In: Development of Computational Models (DCM2014), 2014, Viena. Pre-Proceedings of DCM 2014, 2014. p. 1-10.
NALON, C. ; VIEIRA, B. L. ; DOWEK, G. ; HAEUSLER, E. H. . A Calculus for Automatic Verification of Petri Nets based on Resolution and Dynamic Logics. In: LSFA 2014, 2014, Brasília. Pre-proceedings of the LSFA 2014. Brasília: CIC-UnB, 2014. p. 95-110.
ENGLANDER, C. ; DOWEK, G. ; HAEUSLER, E. H. . Yet Another Bijection Between Sequent Calculus and Natural Deduction. In: LSFA 2014, 2014, Brasília. Pre-proceedings of the LSFA 2014. Brasília: CIC-UnB, 2014. p. 75-90.
Hausler, E. H. . How many times do we need an assumption to prove a tautology in Minimal logic: An example on the compression power of Classical reasoning. In: Ninth Latin American Workshop on Logic/Languages, Algorithms and New Methods of Reasoning, LANMR2014, 2014, Valle de Bravo, México. Proceedings of Ninth LANMR. Aachen: CEUR-Workshops, 2012. v. 1287. p. 1-12.
PINHEIRO, V. ; ENDLER, M. ; HAEUSLER, E. H. . A Framework for Customizing the Mobile and Remote Monitoring of Patients with Chronic Diseases. In: IEEE 16th International Conference on E-health Networking, Application & Services (Healthcom), 2014, Natal. Proceedings of A Framework for Customizing the Mobile and Remote Monitoring of Patients with Chronic Diseases. Los Alamitos: IEEE, 2014. p. 259-264.
CRUZ, M. Q. ; HAEUSLER, E. H. . Proof-graphs for Minimal Implicational Logic. In: Developments in Computational Models, CONCUR2013, 2013, Argentina. Preliminary Proceedings (Pre-proceedings), 2013. p. 15-24.
PINHEIRO, V. ; ENDLER, M. ; HAEUSLER, E. H. . Customized mobile monitoring for patients with chronic diseases (short paper). In: 5th International Conference on eHealth, Telemedicine, and Social Medicine (eTELEMED 2013), 2013, Nice. Proceedings of the 5th International Conference on eHealth, Telemedicine, and Social Medicine (eTELEMED 2013), 2013.
TELES, A. ; PINHEIRO, D. ; GONCALVEZ, J. F. ; BATISTA, R. ; SILVA, F. ; PINHEIRO, V. ; Haeusler, Edward H. ; ENDLER, M. . MobileHealthNet: A Middleware for Mobile Social Networks in m-Health. In: 3rd International Conference on Wireless Mobile Communication and Healthcare (MOBIHEALTH 2012), 2012, Paris. Proccedings of the 3rd International Conference on Wireless Mobile Communication and Healthcare (MOBIHEALTH 2012), 2012.
PINHEIRO, V. ; ENDLER, M. ; Haeusler, Edward H. . Acompanhamento remoto movel customizavel de pacientes com doenç?as crônicas. In: XIII Congresso Brasileiro de Informatica em Saude, 2012, Curitiba. Proceedings of the XIII Congresso Brasileiro de Informatica em Saude, 2012.
HAEUSLER, E. H. ; PAIVA, V. ; RADEMAKER, A. . Intuitionistic Description Logic and Legal Reasoning. In: DALI 2011 - DEXA workshops, 2011, Toulouse. 22nd Database and Expert Systems Applications: International Workshops. Los Alamitos: IEEE Computer Society, 2011. p. 345-349.
VIEIRA, B. L. ; BENEVIDES, M. R. F. ; HAEUSLER, E. H. . Propositional Dynamic Logic for Petri Nets.. In: 6th Workshop on Logical and Semantic Frameworks, 2011, Belo Horizontes. Proceedings of the 6th Workshop on Logical and Semantic Frameworks, 2011.
HAEUSLER, E. H. ; RADEMAKER, A. ; PAIVA, V. . Using Intuitionistic Logic as a basis for Legal Ontologies. In: 4th Workshop on Legal Ontologies and Artiﬁcial Intelligence Techniques, 2010, Firenze. CEUR Workshop Proceedings, 2010. v. 605. p. 69-76.
PAIVA, V. ; RADEMAKER, A. ; HAEUSLER, E. H. . Constructive Description Logic, Hybrid Style. In: Hylo2010. Hybrid Logic Workshop. FLOCS 2010, 2010, Edinburgh. Pre-proceedings, 2010.
ENGLANDER, C. ; HAEUSLER, E. H. . On the 2-Categorical View of Proofs. In: ISoLA 2010 - 4th International Symposium On Leveraging Applications of Formal Methods, 2010., 2010, Amirandes, Heraclion, Crete. Lectures Notes in Computer Science - Leveraging Applications of Formal Methods, Verification and Validation. Heidelberg: Springer-Verlag, 2010. v. 6415. p. 508-518.
HAEUSLER, E. H. ; PAIVA, V. ; RADEMAKER, A. . Intuitionistic Logic and Legal Ontologies. In: JURIX 2010: The 23rd International Conference on Legal Knowledge and Information Systems., 2010, Liverpool. Frontiers of Artificial Intelligence and Applications. Amsterdam: IOS Press, 2010. p. 155-158.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. . Algebraic Framework for Reverse Engineering on Specifications. In: IV Congress on Logic Applied to Technology, 2009, Santos. Advances in Technological Applications of Logical and Intelligent Systems - Selected Papers from the Sixth Congress on Logic Applied to Technology. Amsterdam: IOS Press, 2009. v. 186. p. 1-12.
FERNANDES, R. ; HAEUSLER, E. H. . A Topos-Theoretic Approach to Counterfactual Logic. In: Fourth Workshop on Logical and Semantic Frameworks, with Applications, 2009, Brasília. Pre-proceedings. Brasília: UnB, 2009.
COSTA, V. G. ; SANZ, Wagner ; HAEUSLER, E. H. ; PEREIRA, L. C. . Peirce's rule in a full Natural Deduction system. In: Fourth Workshop on Logical and Semantic Frameworks, with Applications, 2009, Brasilia. Pre-proceedings. Brasilia: UnB, 2009.
GUEDES, L. C. C. ; HAEUSLER, E. H. . Action Algebras and Model Algebras in Denotational Semantics. In: PDM09, 2009, Udine. Peter Mosses Festschirifft. Berlim: Springer-Verlag, 2009. v. 5700. p. 227-249.
BRAGA, C. O. ; HAEUSLER, E. H. . Programming Games and their Equilibria in Maude.. In: RULE09 The Tenth International Workshop on Rule-Based Programming, 2009, Brasília. Pre-proceedings. Brasília: UNB, 2009.
CAFEZEIRO, I. L. ; VITERBO, J. ; RADEMAKER, A. ; Haeusler, Edward Hermann ; ENDLER, M. . Designing Ubiquitous Applications: A Proposal of Architecture for Specification Environment. In: 6th IEEE International Workshop on Managing Ubiquitous Communications and Services (MUCS 2009),, 2009, Barcelona. Proc. of 6th IEEE International Workshop on Managing Ubiquitous Communications and Services (MUCS 2009),. USA: IEEE, 2009.
RADEMAKER, A. ; Hæusler, Edward Hermann . Is it important to explain a theorem ? A case study on UML and ALCQI. In: ETHECOM - ER, 2009, Gramado. Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2009. v. 5833. p. 33-44.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. ; RADEMAKER, A. . Ontology and Context. In: 5th IEEE Workshop on Context Modeling and Reasoning (CoMoRea) co-Located with PerCom2008., 2008, Hong Kong. Proceedings. Los Alamitos: IEEE, 2008.
VASCONCELOS, D. R. ; HAEUSLER, E. H. . Towards an Implementation Theory via a Game Logic Approach. In: 8th Conference on Logic and the Foundations of Game and Decision Theory, 2008, Amsterdam. Pre-Proceedings. Amsterdam: UVA, 2008.
RADEMAKER, A. ; HAEUSLER, E. H. . Toward Short and Structural ALC-Reasoning Explanations: A Sequent Calculus Approach. In: SImpósio Brasileiro de Inteligência Artificial, 2008, Salvador. LNAI. Berlim: Springer-Verlag, 2008. v. 5249. p. 167-176.
CAFEZEIRO, I. L. ; VITERBO, J. ; RADEMAKER, A. ; HAEUSLER, E. H. ; ENDLER, M. . A Formal Framework for Modeling Context-Aware Behavior in Ubiquitous Computing. In: ISOLA 2008, 2008, Kassandra Grécia. Communications in Computer and Information Science. |Berlim: Springer-Verlag, 2008. v. 17. p. 519-533.
MARTINS, C. B. ; HAEUSLER, E. H. . Automatic Parallel Code Generation through Denotational Semantics and Dependence Graphs. In: II workshop on Languages and Tools for Parallel and Distributed Programming (LTPD 2008), 2008, Fortaleza. Proceedings of LTPD 2008. Fortaleza: Editora-UFC, 2008.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. . Semantics Interoperability via Category Theory. In: ER 2007, 2007, Auckland. Proc. Tutorials, posters, panels and industrial contributions at the 26th International Conference on Conceptual Modeling - ER 2007. Auckland: CRPIT, 2007. v. 83. p. 197-202.
VASCONCELOS, D. R. ; HAEUSLER, E. H. . Reasoning about Games via a First-order Modal Model Checking. In: Simpósio Brasileiro de Métodos Formais, 2007, Ouro Preto. Proceedings of SBMF 2007. Ouro Preto: Universidade de Ouro Preto - SBC, 2007.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. . Algebraic Framework for Reverse Engineering on Specifications. In: VI Congress of Logic Applied to Technology, 2007, Santos. Proceedeings LAPTEC. Santos: SENAC-SBC, 2007.
IMPERIAL, J. C. ; HAEUSLER, E. H. . Trust in Intelligent Agents. In: LAACS, 2007, Petrópolis. Proceedings of LAACS 2007. Los Alamitos: IEEE, 2007.
DUARTE, A. R. ; HAEUSLER, E. H. ; RIBEIRO, C. C. ; URRUTIA, S. . Referee Assignment in Sports Tournaments. In: The 6th International Conference on the Practice and Theory of Automated Timetabling, 2007, Brno. Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2007. v. 3867. p. 158-173.
SILVA, G. M. H. ; RADEMAKER, A. ; VASCONCELOS, D. R. ; AMARAL, F. N. ; MARTINS, C. B. ; COSTA, V. G. ; HAEUSLER, E. H. . Dealing with the Formal Analysis of Information Security Policies through Ontologies: A Case Study. In: Australasian Ontology Workshop, 2007, Surfers Paradise. proceedings of AOW-07. Melbourne: CRPIT- Australian Computer Society, 2007. v. 85.
HAEUSLER, E. H. ; VASCONCELOS, D. R. ; BENEVIDES, M. R. F. . Defining Agents via Strategies: Towards a Game-Theoretical view of MAS. In: Workshop on Radical Agent Concepts, 2006, Washington. Lecture Notes in Artificial Inteligence. London: Springer-Verlag, 2006. v. 3825. p. 299-311.
AMARAL, F. N. ; MARTINS, C. B. ; SILVA, G. M. H. ; RADEMAKER, A. ; HAEUSLER, E. H. . An Ontology-based Approach to the Formalization of Information Security Policies. In: VORTE-EDOC, 2006, HONG-KONG. Proceedings of VORTE-EDOC. Los Alamitos, USA: IEEE Communications Society, 2006. p. 20-28.
WOLTER, U. ; MARTINI, A. ; HAEUSLER, E. H. . Indexed General Logics. In: Logical and Semantic Frameworks with Applications, 2006, Natal. Pre-Proceedings. NATAL: UFRN, 2006.
AMARAL, F. N. ; HAEUSLER, E. H. . Topos-Based Logical Frameworks and an Application to (Meta)Heuristic Search. In: Logical and Semantic Frameworks with Applications, 2006, Natal. Pre-Proceedings. Natal: UFRN, 2006.
CORRÊA, M. S. ; HAEUSLER, E. H. . On the Selective Lambek Calculus. In: Logical Aspects of Computational Linguistics, 5th International Conference, 2005, Bordeaux. Lecture Notes in Computer Science. Berlim: Springer-Verlag, 2005. v. 3492. p. 67-83.
HAEUSLER, E. H. ; MARTINS, C. B. ; ENDLER, M. . Language-Oriented Formal Analysis: a Case Study on Protocols and Distributed Systems. In: SBMF, 2005, Porto Alegre. Proceedings of the Brazilian Symposim on Formal Methods 2005. Amsterdam: Elsevier, 2005.
MARTINS, C. B. ; HAEUSLER, E. H. ; ENDLER, M. . Binding Network Topologies to Specifications via Pronouns. In: II South-West European Workshop on Formal Methods, 2005, Orhid. Proceedings, 2005.
RENTERIA, C. J. ; HAEUSLER, E. H. . A Natural Deduction for Keisler Quantification. In: WOLLIC, 2004, PARIS. Proceedings of WOLLIC. Amsterdam: Elsevier, 2004.
HAENDCHEN FILHO, A. ; CAMINADA, N. ; HAEUSLER, E. H. ; STAA, A. V. . Facilitating the Process of Specification Capture and Transformation on the Formal Development of Multi-Agent Systems. In: FAAB NASA 2004, 2004, Washington. Proceedings. Washington: IEEE, 2004.
BREITMAN, K. K. ; HAENDCHEN FILHO, A. ; HAEUSLER, E. H. ; STAA, A. V. . Using Ontologies to Formalize Service Specification in Multi-Agent Systems. In: FAAB NASA 2004, 2004, Washington. Proceedings, 2004.
IMPERIAL, J. C. ; HAEUSLER, E. H. . Some Strategies for the Automatic Use of Hoare Logic. In: STRATEGIES'04, 2004, CORCH. Proceedings of STRATEGIES'2004. Amsterdã - Holanda: Elsevier, 2004.
VASCONCELOS, D. R. ; HAEUSLER, E. H. . A Logic View of Playing Games. In: LAPTEC, 2003, Marília-SP. Advances in Logic, Artificial Intelligence and Robotics. Holanda: IOS Press, 2003. v. 101.
SPINOLA, A. I. A. ; HAEUSLER, E. H. . Anticipatory Topoi. In: CASYS'2001, 2002, Liege-Belgium. Computing Anticipatory Systems (CASYS). Melville NY: American Institute of Physics, 2002.
BRAGA, C. O. ; HAEUSLER, E. H. ; MESEGUER, J. ; MOSSES, P. D. . Mapping Modular SOS to Rewriting Logic. In: LOPSTR'2002, 2002, Madrid. Proceedings of LOPSTR'2002 , Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2002.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. . Categorical Limits in Reuse of Algebraic Specification. In: LAPTEC'2002, 2002, São Paulo. Frontiers of Artificial Intelligence and its Applications. Amsterdã: IOS Press, 2002.
SILVA, G. M. H. ; HAEUSLER, E. H. ; VELOSO, P. A. S. . Constructive Program Synthesis using Intuitionistic Logic and Natural Deduction. In: LAPTEC'2002, 2002, São Paulo. Frontiers of Artificial Intelligence and its Applications. Amsterdã: IOS Press, 2002.
AMARAL, F. N. ; HAEUSLER, E. H. ; ENDLER, M. . A Real-Time Specification Language. In: LAPTEC'2002, 2002, São Paulo. Frontiers of Artificial Intelligence and its Applications. Amsterdã: IOS Press, 2002.
MARTINI, A. ; HAEUSLER, E. H. ; WOLTER, U. . A Taste on Putting Logical Systems Together. In: Workshop de Métodos Formais, 2001, Rio de Janeiro. Proceedings of the IV WMF. Rio de Janeiro: SBC, 2001.
MARTINI, A. ; WOLTER, U. ; HAEUSLER, E. H. ; VIZZOTO, J. . Linking Logics for Multiparadigm Software Specification. In: SCI2001, 2001, Orlando. Proceedings of the 5th World Multiconference on Systems Cybernetics and Informatics. Miami: IIIS Press, 2001.
GUEDES, L. C. C. ; HAEUSLER, E. H. . A Formal Approach for Specifying XML-based Languages. In: Simpósio Brasileiro de Linguagens de Programação, 2001, Curitiba - Paraná. Anais do V SBLP. Curitiba: Universidade Federal do Paraná, 2001.
MARTINI, A. ; WOLTER, U. ; HAEUSLER, E. H. . Reasons and Ways to Cope with a Spectrum of Logics. In: LAPTEC'2001, 2001, São Paulo. Frontiers of Artificial Intelligence and its Applications. Amsterdã: IOS Press, 2001.
BRAGA, C. O. ; HAEUSLER, E. H. ; MESEGUER, J. ; MOSSES, P. D. . Using Reflection to Map Action Semantics to Rewriting Logics. In: AMAST'2000, 2000, IOWA. LNCS. Nova Iorque: Springer-Verlag, 2000. v. 1816. p. 126-141.
De MOURA, L. ; LUCENA, C. J. P. ; HAEUSLER, E. H. . Analysis of Parallel Programs. In: Simpósio Brasileiro de Linguagens de Programação, 2000, Recife. Proceedings do IV SBLP, 2000. p. 106-119.
De MOURA, L. ; LUCENA, C. J. P. ; HAEUSLER, E. H. . A modular implementation of Action Notation. In: Workshop on Action Semantics, 2000, Recife. Proceedings. Aarhus - Dinamarca: BRICS, 2000. p. 23-34.
GARCIA, Alex V. ; HAEUSLER, E. H. . Um Modelo Categórico para Tradução entre Linguagens de Programação. In: Simpósio Brasileiro de Linguagens de Programação, 2000, Recife. Proceedings do IV SBLP. Recife: SBC-UFPE, 2000. p. 62-75.
SPINOLA, A. I. A. ; HAEUSLER, E. H. . A study on semi-sheaves associated to transition systems representing reactive systems. In: Workshop on Geometry and Topology in Concurrency, 2000, Pensylvania. Proceedings. Nova Iorque: Elsevier, 2000. p. 1-16.
AMARAL, F. N. ; HAEUSLER, E. H. . Completeness of an Action Logic Featuring a delta-Operator for Timed Transition Systems. In: WOLLIC, 2000, Recife. Proceedings. Recife: FOLLIC, UFPE, 2000.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. . Sharing in Denotational Semantics. In: Workshop de Métodos Formais, 2000, João Pessoa - PB. Proceedings do WMF2000, 2000. p. 145-156.
SILVA, G. M. H. ; HAEUSLER, E. H. . Síntese Construtiva de Programas Utilizando Lógica Intuicionista. In: Workshop de Métodos Formais, 2000, João Pessoa - PB. Proccedings do WMF2000. João Pessoa - PB: SBC, 2000. p. 55-67.
AMARAL, F. N. ; HAEUSLER, E. H. . A Logic-Based Approach for Real-Time Object-Oriented Software Development. In: Workshop de Métodos Formais, 2000, João Pessoa - PB. Proceedings do WMF2000. João Pessoa - PB: SBC, 2000. p. 45-55.
FÉLIX, M. F. ; HAEUSLER, E. H. . LET: Uma Linguagem para especificar Transformações. In: III Simpósio Brasileiro de Linguagens de Programação, 1999, Porto Alegre. Anais. Porto Alegre: Editora da SBC, 1999. v. 1. p. 109-124.
HAEUSLER, E. H. ; FONTOURA, M. F. . Using Transition Systems to Formalize a Pattern for Time Dependable Applications. In: IEEE Workshop on Object-Oriented Time-Dependable Systems, 1999, Santa Barbara. Proceedings of the Fourth International Workshop on Object-Oriented Time-Dependable Systems. Piscataway, NJ: IEEE Computer Society, 1999. v. 1. p. 216-227.
CORRÊA, M. S. ; HAEUSLER, E. H. . The Selective Lambek Syntactic Calculus. In: Workshop on Logic Language and Information, 1998, São Paulo. Proceedings of the 5th WOLLIC. Sao Paulo: EDUSP, 1998. p. 96-108.
ALMEIDA, E. S. ; HAEUSLER, E. H. . Lorec: A Resource Sensitive Logic Based On Petri Nets. In: I Workshop de Metodos Formais, 1998, Porto Alegre. Proceedings. Porto Alegre: Editora da UFRGS, 1998. p. 10-19.
BRAGA, C. O. ; FONTOURA, M. F. ; HAEUSLER, E. H. ; LUCENA, C. J. P. . Formalizing OO Frameworks and Frameworks Instantiation. In: Workshop de Métodos Formais, 1998, Porto Alegre. Proceedings. Porto Alegre: Editora da UFRGS, 1998. p. 100-105.
CARVALHO, S. E. R. ; FIADEIRO, J. L. L. ; HAEUSLER, E. H. . A Formal Approach To Real-Time Object Oriented Software. In: IFAC WORKSHOP ON REAL-TIME PROGRAMMING, 1997, Lyon. PROCEEDINGS. Londres: Pergamon, 1997. v. 1. p. 91-96.
GARCIA, Alex V. ; HAEUSLER, E. H. ; HAERBERER, A. . A Semantic Approach To The Solution For The Legacy Code Problem. In: FORMAL METHODS PACIFIC, 1997, Wellington. PROCEEDINGS. WELLINGTON, NOVA ZELANDIA: Univeristy of Wellington, 1997.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. ; HAERBERER, A. . From Diagram To Code Via Attribute Grammar. In: II Simpósio Brasileiro de Linguagens de Programação, 1997, Campinas. ANAIS. CAMPINAS: Editora da Unicamp, 1997. v. 1. p. 165-178.
GARCIA, Alex V. ; HAEUSLER, E. H. ; HAERBERER, A. . An Architecture For Semantically Based Code Migration. In: II Simpósio Brasileiro de Linguagens de Programação, 1997, Campinas. ANAIS. CAMPINAS: Editora da UNICAMP, 1997. p. 179-192.
GARCIA, Alex V. ; HAEUSLER, E. H. . Towards A Categorical Model For Language Translation. In: II Simpósio Brasileiro de Banco de Dados, 1997, Campinas. ANAIS. CAMPINAS: Editora da Unicamp, 1997. p. 193-203.
GARCIA, Alex V. ; HAEUSLER, E. H. ; HAERBERER, A. . A semantic Approach to the Solution of Legacy Code Problem. In: Formal Methods Pacific, 1997, Wellington. Formal Methods Pacific. Nova Iorque: Springer-Verlag, 1997. p. 299-310.
ABOIM, D. S. ; HAEUSLER, E. H. ; SOUZA, C. S. . Structured Argument In A Logic-Based Kb-System. In: ITALLC MEETING, 1996, Indiana. ANAIS. INDIANA, EUA: University of Indiana, 1996.
MAIA, A. C. P. ; HAEUSLER, E. H. ; LUCENA, C. J. P. . A Model For Cooperative Software Design. In: INTERNATIONAL SYMPOSIUM ON DESCRIPTIVE MODELS ON DESIGN, 1996, Istambul. ANAIS. Londres: kluwer, 1996. p. 103-118.
HAEUSLER, E. H. . Integrating Functional And Logic Languages: A Denotational Approach. In: THIRD MASSEY FUNCTIONAL PROGRAMMING WORKSHOP, 1996, Palmstrom North. ANAIS. MASSEY, NOVA ZELANDIA: International Universty of New Zealand, 1996. v. 1. p. 55-64.
CORRÊA, M. S. ; HAEUSLER, E. H. ; PAIVA, V. . A Dialectica Model Of State. In: CATS'96, 1996, Melbourne. ANAIS. MELBOURNE, AUSTRALIA: University of Melbourne, 1996. v. 18. p. 29-37.
CAFEZEIRO, I. L. ; HAEUSLER, E. H. ; LUCENA, C. J. P. . A Geometric Approch To The Definition Of Programming Languages. In: I SBLP, 1996, Belo Horizonte. ANAIS. BELO HORIZONTE, MG: Ed. UFMG, 1996. v. 1. p. 265-276.
GUEDES, L. C. C. ; HAEUSLER, E. H. . On The Separability Of Denotational Semantics. In: I Simpósio Brasileiro de Linguagens de Programação, 1996, Belo Horizonte. ANAIS. BELO HORIZONTE, MG: Editora da UFMG, 1996. v. 1. p. 209-222.
GUEDES, L. C. C. ; HAEUSLER, E. H. ; RANGEL, J. L. M. . An Object Oriented Model For Semantics Directed Compiler Generation. In: I SBLP, 1996, Belo Horizonte. ANAIS. BELO HORIZONTE, MG: Editora da UFMG, 1996. v. 1. p. 155-168.
FRIAS, M. F. ; MERE, M. C. ; HAEUSLER, E. H. ; PEREIRA, L. C. . Multiplicative Quantifiers In Linear Logic: Proof Theory And Algebraic Semantics. In: I LPDPL, 1995, Darmstadt. ANAIS. DARMSTADT, ALEMANHA: University of Darmstadt, 1995.
MERE, M. C. ; HAEUSLER, E. H. ; FRIAS, M. F. ; PEREIRA, L. C. . Bounded Paralell Linear Logic. In: WINTER MEETING OF THE AMERICAN MATHEMATICAL SOCIETY, 1995, São Francisco. ANAIS. New York: ASL, 1995.
GUEDES, L. C. C. ; HAEUSLER, E. H. ; RANGEL, J. L. M. . Object Oriented Semantics Directed Compiler Generation: A Prototype. In: TAPSOFT'95, 1995, Aarhus. ANAIS. Berlim: Springer-Verlag, 1995. v. 917. p. 957-958.
HAEUSLER, E. H. ; PAZ, A. C. . A Natural Deduction Theorem Proving Generator. In: XI SIMPOSIO BRASILEIRO DE INTELIGENCIA ARTIFICIAL, 1994, Fortaleza. ANAIS. FORTALEZA, CE: Universidade Federal de Fortaleza, 1994. v. 1. p. 557-571.
ALMEIDA, E. S. ; HAEUSLER, E. H. . Utilizacao de CSP Como ferramenta Para Especificacao de Linguagens Orientadas A Objetos. In: XIV SEMISH, 1994, Caxambu. ANAIS. CAXAMBU, MG: ED. SBC, 1994. v. 1. p. 324-339.
HAEUSLER, E. H. . A Theorem Prover Based On Game Theoretic Semantics.. In: Conferencia Internacional sobre Informatica, 1988, La Habana. LA HABANA - CUBA, 1988. p. 13-26.
HAEUSLER, E. H. . Explanation By Game.. In: PROCEEDINGS OF THE ITS-88 INTERNATIONAL CONFERENCE., 1988, Montreal. Proceedings. MONTREAL-CANADA: ACM, 1988. p. 76-86.
HAEUSLER, E. H. ; PEQUENO, T. H. C. . Um Provador de Teoremas Baseado Em Jogos Semanticos.. In: IV SIMPOSIO BRASILEIRO DE I.A., 1987, Ubêrlandia. ANAIS DO IV SIMPOSIO BRASILEIRO DE I.A.. UBERLANDIA - MG: SBC, 1987. p. 54-68.
RADEMAKER, A. ; HAEUSLER, E. H. . An Intuitionisticaly based Description Logic. In: Third Gentzen Systems and Beyond workshop, 2014, Viena. Proceedings of GSB 2014, 2014. p. 1-5.
RADEMAKER, A. ; HAEUSLER, E. H. ; PEREIRA, L. C. . On the Proof Theory of ALC. In: Brazilian Logic Conference, 2008, Paraty. Pre-Proceedings. Campinas: Unicamp, 2008.
WOLTER, U. ; MARTINI, A. ; HAEUSLER, E. H. . Indexed Logical Closure Operators. In: Brazilian Logic Conference, 2008, Paraty. Pre-Proceedings. Campinas: Unicamp, 2008.
VASCONCELOS, D. R. ; HAEUSLER, E. H. . Quantifying in Extensive Games. In: Brazilian Logic Conference, 2008, Paraty. Pre-Proceedings. Campinas: Unicamp, 2008.
PINHEIRO, V. ; SILVA, G. M. H. ; SOSSAI, J. ; Haeusler, Edward Hermann . Aplicação de ontologias na extração de informações de modelos hidrodinâmicos: Sistema baseado em conhecimento. In: Seminário de Pesquisa em Ontologia, 2008, Niterói. Anais do I Seminário de Pesquisa em Ontologias, 2008.
VASCONCELOS, D. R. ; HAEUSLER, E. H. ; BENEVIDES, M. R. F. . Reasoning about Games via Temporal Logic. In: 7th Augustus deMorgan Workshop, 2005, Londres. Proceedings. Amsterdam: UVA.
MACEDO, H. ; HAEUSLER, E. H. . Yoneda?s embedding and Post-completeness. In: GetFun2.0, 2014, Viena. Proceedings of GetFun2.0, 2014. p. 1-5.
ENGLANDER, C. ; HAEUSLER, E. H. . Natural deduction for non-deterministic finitely many-valued logics. In: GetFun2.0, 2014, Viena. Proceedings of GetFun2.0, 2014. p. 1-1.
RADEMAKER, A. ; HAEUSLER, E. H. . An intuitionistic ALC description default logic. In: GetFun2.0, 2014, Viena. Proceedings of GetFun2.0, 2014. p. 1-1.
SANTOS, J. ; VIEIRA, B. L. ; CRUZ, M. Q. ; Haeusler, Edward H. . Improving memory performance for mimp-graph based theorem provers. In: Latin American Symposium on Mathematical Logic, 2014, Buenos Aires. Abstracts of the 16th Latin American Symposium on Mathematical Logic, 2014.
VELOSO, P. A. S. ; PEREIRA, L. C. ; HAEUSLER, E. H. . ON WHAT MUST BE: Existential Validities and some Related Riddles.. In: Logic Colloquium, 2010, Paris. Book of Abstracts of Logic Colloquium, 2010.
PEREIRA, L. C. ; HAEUSLER, E. H. ; COSTA, V. G. ; SANZ, Wagner . Revisiting Peirce's Rule in Natural Deduction. In: Logic Coloquium, 2008, Berna-Suíça. Volume of Abstracts of Logic Coloquium 2008. New York: Association for Symbolic Logic, 2008.
WOLTER, U. ; MARTINI, A. ; HAEUSLER, E. H. . General Indexed Logics. In: Universal Logic, 2007, Xi'an. Handbook of UNILOG2007. Beijing: NYP, 2007. p. 15-15.
PEREIRA, L. C. ; HAEUSLER, E. H. . On the Relationship between Structural Reductions and the Identity Problem. In: Universal Logic, 2007, Xi'an. Handbook of UNILOG2007. Beijing: NPU, 2007. p. 74-74.
PEREIRA, L. C. ; HAEUSLER, E. H. . On Some Relations Between Fragments of Classical and Intuitionistic Logic. In: 13th International Congress of Logic, Methodology and Philosophy of Science, 2007, Beijing. Volume of Abstracts. Beijing: Division of Logic, Methodology and Phylosophy of Science of the International Union on Phil. of Sci., 2007. p. 69-69.
VASCONCELOS, D. R. ; HAEUSLER, E. H. . Quantifying in Games. In: GAMES 2007 Annual Meeting, 2007, Lausanne. Volume of Abstracts. Lausanne: University of Lausanne, 2007.
VASCONCELOS, D. R. ; HAEUSLER, E. H. . Towards an Implementation Theory of Games. In: GAMES 2007 Annual Meeting, 2007, Lausanne. Volume of Abstracts. Lausanne: University of Lausanne, 2007.
MARTINI, A. ; WOLTER, U. ; HAEUSLER, E. H. . Fibred and Indexed Categories for Abstract Model Theory. In: Encontro Brasileiro de Lógica, 2006, Itatiaia. Proceedings. CAMPINAS: UNICAMP.
COSTA, V. G. ; HAEUSLER, E. H. . On Strategies to Compact Proofs. In: Encontro Brasileiro de Lógica, 2006, Itatiaia. Proceedings. CAMPINAS: UNICAMP.
AMARAL, F. N. ; HAEUSLER, E. H. . Using the Internal Logic of a Topos Related to the Topos of Forest to Model Search Spaces for Problems. In: Encontro Brasileiro de Lógica, 2006, Itatiaia. Proceedings. CAMPINAS: UNICAMP.
HAEUSLER, E. H. ; CORRÊA, M. S. . On Games and the Polynomial Completeness of Intuitionistic Logic. In: Encontro Brasileiro de Lógica, 2006, Itatiaia. Proceedings. CAMPINAS: UNICAMP.
HAEUSLER, E. H. ; PEREIRA, L. C. . Structural Reductions and the Identity Problem. In: XIII Latin Amerin Simposium on Mathematical Logic, 2006, Oaxaca, México. Proceedings. Rhode Island, EUA: ASL.
IMPERIAL, J. C. ; HAEUSLER, E. H. . Strategies for the Semi-Automatic Use of Hoare Logic. In: Encontro Brasileiro de Lógica, 2006, Itatiaia. Proceedings. CAMPINAS: UNICAMP.
COSTA, V. G. ; HAEUSLER, E. H. ; LABER, E. S. ; NOGUEIRA, L. . A note on the size of minimal covers. In: 19th INternational Symposium on Mathematical Programming, 2006, Rio de Janeiro. Proceedings, 2006.
HAEUSLER, E. H. ; MARTINI, A. . Maps and universal constructions for interoperability of logical theories. In: Universal Logic 2005, 2005, Montreaux. Logica Universalis. Genebra: Birkhauser, 2005. v. 1.
RENTERIA, C. J. ; HAEUSLER, E. H. ; VELOSO, P. A. S. . Natural Deduction for Ultra-Filter Logic. In: Encontro Brasileiro de Logica, 2003, Campinas. Proceedings. Campinas: Unicamp, 2003.
SILVA, G. M. H. ; HAEUSLER, E. H. ; VELOSO, P. A. S. . Exploring the Computational Content of INtuitionistic Proofs. In: Encontro Brasileiro de Logica, 2003, Campinas. Proceedings. Campinas: Unicamp, 2003.
RENTERIA, C. J. ; HAEUSLER, E. H. . A Natural Deduction for CTL. In: Logic Coloquium 2000, 2000, Paris. Proceedings. Paris: La Sorbonne, 2000. p. 37-37.
AMARAL, F. N. ; HAEUSLER, E. H. . An Action Logic for Real-Time Reasoning. In: Logic Coloquium 2000, 2000, Paris. Proceedings. Paris: La Sorbonne, 2000. p. 223-223.
MORETH, R. C. ; PEREIRA, L. C. ; HAEUSLER, E. H. . A New Cut-Free Calculus For S5. In: X Latin-American Symposyum on Mathematical Logic, 1998, Merida. Proceedings. Merida- Venezuela: Editora da Universidade de los Andes, 1998.
CORRÊA, M. S. ; HAEUSLER, E. H. . A Lazy Lambek Calculus. In: Logic Coloquim'98, 1998, Praga. Proceedings. Paris: Editora da Universidade de Paris VII, 1998.
HAEUSLER, E. H. . Quantifiers, Adjunctions And L-Sets. In: Latin American Symposium on Mathematical Logic, 1997, Salvador. Logic Journal of IGPL. Oxford, 1997. v. 5. p. 456-457.
FIGUEIREDO, L. C. ; HAEUSLER, E. H. . A Computational Interpretation Of Proof Nets With Trips. In: LOGIC COLOQUIUM'94, 1994, Clermont Ferrant. ANAIS. Paris: University of Paris, 1994.
HAEUSLER, E. H. ; PEREIRA, L. C. . A Calculus For Purely Exponential Linera Logic-Abstract. Logic Journal of IGPL, Oxford, v. 5, n.3, p. 457-457, 1997.
MERE, M. C. ; HAEUSLER, E. H. ; FRIAS, M. F. ; PEREIRA, L. C. . Multiplicative Quantifiers In Linear Logic - Abstract. BULLETIM OF THE ASSOCIATION FOR SYMBOLIC LOGIC, RHODE ISLAND, ENGLAND, v. 1, n.1, 1995.
COSTA, V. G. ; HAEUSLER, E. H. . Comutational Manifolds. Studia Logica , 2025.
Hæusler, Edward Hermann . Huge proofs are Redundant. 2024. (Apresentação de Trabalho/Conferência ou palestra).
Cucolato, B. ; SANTOS, J. B. ; Haeusler, Edward Hermann . A labelled Natural Deduction logical framework. 2024. (Apresentação de Trabalho/Conferência ou palestra).
CALLOU, R. ; Hæusler, Edward Hermann . Soundness of the Horizontal Compression in Lean. 2024. (Apresentação de Trabalho/Conferência ou palestra).
ALKMIN, B. ; NALON, C. ; Haeusler, Edward Hermann . A Natural Deduction System Aimed at Explainability. 2024. (Apresentação de Trabalho/Conferência ou palestra).
SARAIVA, L. ; Hæusler, Edward Hermann ; COSTA, V. G. . Quantum Algorithm for Multiplicative Linear Logic. 2024. (Apresentação de Trabalho/Outra).
Hæusler, Edward Hermann . Solomonoff-Based Framework for Explainability in Machine Learning. 2024. (Apresentação de Trabalho/Conferência ou palestra).
Hæusler, Edward Hermann . 'Short proofs for non-Hamiltonian graphs through quantum computing'. 2024. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward H. ; Lassale Casanave, A. ; GIOVANNINI, E. . On De Zolt?s Postulate in Three-Dimensional Geometry.. 2023. (Apresentação de Trabalho/Conferência ou palestra).
SARAIVA, L. ; COSTA, V. G. ; Hausler, E. H. . Quantum Algorithm for Multiplicative Linear Logic. 2022. (Apresentação de Trabalho/Simpósio).
Haeusler, Edward Hermann . The role of finiteness in the foundations of mathematics and computation. 2021. (Apresentação de Trabalho/Conferência ou palestra).
Cucolato, B. ; DE BARROS SANTOS, JEFFERSON ; Haeusler, Edward H. . A logical framework with a graph meta-language. 2021. (Apresentação de Trabalho/Congresso).
SLAVIERO, C. ; Haeusler, Edward H. . A-Games: using game-like representation for representing finite automata. 2021. (Apresentação de Trabalho/Congresso).
Gordeev, L. ; Haeusler, Edward Hermann . On Proof Theory in Computational Complexity. 2021. (Apresentação de Trabalho/Simpósio).
ALKMIM, B. P. ; Haeusler, Edward Hermann ; SCHWABE, D. . Reasoning over Knowledge Graphs in an Intuitionistic Description Logic. 2020. (Apresentação de Trabalho/Congresso).
GIOVANNINI, E. ; Lassale Casanave, A. ; VELOSO, P. A. S. ; Haeusler, Edward H. . Zolt's Postulate in Higher Dimension (Indircernability, Cauchy Integrals, Waves and Sheaves). 2019. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward H. . Redundancy in huge Natural Deduction proofs. 2019. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward H. . Proof, Computaion and Complexity: a Critical Analysis. 2019. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward H. . Huge proofs are highly redundant: An argument in favor of NP=PSPACE. 2019. (Apresentação de Trabalho/Comunicação).
ALKMIN, B. ; Haeusler, Edward Hermann ; RADEMAKER, A. . Utilizando iALC para Formalizar a Legislação Brasileira. 2019. (Apresentação de Trabalho/Comunicação).
CAVALCANTE, J. F. B. ; Haeusler, Edward Hermann . Um Estudo Comparativo Sobre Técnicas de Compressão de Provas. 2019. (Apresentação de Trabalho/Comunicação).
COSTA, V. G. ; Haeusler, Edward Hermann . Strong Normalization for Np-Systems via Mimp-Graphs. 2019. (Apresentação de Trabalho/Comunicação).
CALLOU, R. ; Haeusler, Edward Hermann . Using Dependent Type Theory andLE∀Nto prove that every huge normal proof is redundant. 2019. (Apresentação de Trabalho/Comunicação).
Haeusler, Edward Hermann . Redundancy in huge Natural Deduction proofs: Towards an CoNP=NP. 2019. (Apresentação de Trabalho/Comunicação).
HAEUSLER, E. H. . A Discussion on the Received Interpretation of Chaitin's Incompleteness Theorem. 2018. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward Hermann . Proof Compression and the conjecture NP=PSPACE. 2017. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward Hermann . Solving Problems in Intuitionistic Type Theory via General Problem Theory. 2016. (Apresentação de Trabalho/Comunicação).
Haeusler, Edward Hermann ; Gordeev, L. . Compression of proofs and NP vs PSPACE. 2016. (Apresentação de Trabalho/Comunicação).
MACEDO, H. ; Haeusler, Edward Hermann . Yoneda's embedding and Post completeness. 2015. (Apresentação de Trabalho/Comunicação).
CRUZ, M. Q. ; COSTA, V. G. ; Haeusler, Edward Hermann . Np full system and Mimp-fol Association. 2015. (Apresentação de Trabalho/Comunicação).
Haeusler, Edward Hermann ; RADEMAKER, A. . How Kelsenian Jurisprudence and Intuitionistic Logic help to avoid Contrary-to-Duty paradoxes in Legal Ontologies. 2015. (Apresentação de Trabalho/Comunicação).
Haeusler, Edward Hermann . Computational Manifolds and Sheaves. 2015. (Apresentação de Trabalho/Comunicação).
Haeusler, Edward Hermann . Finito Não-Padrão e Modelos Computacionais Formais. 2015. (Apresentação de Trabalho/Conferência ou palestra).
NALON, C. ; VIEIRA, B. L. ; Haeusler, Edward Hermann ; DOWEK, G. . A calculus for automatic verification of Petri Nets based on Resolution and Dynamic Logics. 2014. (Apresentação de Trabalho/Congresso).
Haeusler, Edward Hermann ; BENEVIDES, M. R. F. ; PAIVA, V. ; RADEMAKER, A. . On the Computational Complexity of the Intuitionistic Hybrid Modal Logics. 2014. (Apresentação de Trabalho/Congresso).
SANTOS, J. ; VIEIRA, B. L. ; Haeusler, Edward Hermann . A proof-graphs based theorem prover for Minimal Implicational Logic. 2014. (Apresentação de Trabalho/Congresso).
ENGLANDER, C. ; Haeusler, Edward Hermann ; DOWEK, G. . Correspondence between Natural Deduction and Sequent Calculus. 2014. (Apresentação de Trabalho/Congresso).
HAEUSLER, E. H. . Kelsenian Jurisprudence, legal ontologies and Intuitionistic logic. 2014. (Apresentação de Trabalho/Conferência ou palestra).
HAEUSLER, E. H. . Formal computation models and non-standard finiteness. 2014. (Apresentação de Trabalho/Conferência ou palestra).
HAEUSLER, E. H. . The subformula principle and computational complexity of propositional logics. 2014. (Apresentação de Trabalho/Conferência ou palestra).
Hæusler, Edward Hermann . How relative can be a mathematical concept ? Introducing the duality 'internal versus external' in Category Theory. 2013. (Apresentação de Trabalho/Conferência ou palestra).
Hæusler, Edward Hermann ; MARTINI, A. ; WOLTER, U. . Fibred and Indexed Semantics for a Hoare-like Logic. 2013. (Apresentação de Trabalho/Conferência ou palestra).
Hæusler, Edward Hermann ; MARTINI, A. ; WOLTER, U. . Universality, Naturality and Logical Systems. 2013. (Apresentação de Trabalho/Conferência ou palestra).
Hausler, E. H. . Non-standard Finite Computation. 2013. (Apresentação de Trabalho/Conferência ou palestra).
HAEUSLER, E. H. . A short discussion on non-standard finite computation. 2013. (Apresentação de Trabalho/Conferência ou palestra).
HAEUSLER, E. H. . A proof-theoretical discussion on the mechanization of propositional logics. 2013. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward H. . On the computational complexity of the purely implicational logic. 2012. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward Hermann . A proof theoretical discussion on the mechanization of propositional logic. 2012. (Apresentação de Trabalho/Conferência ou palestra).
Haeusler, Edward Hermann ; PEREIRA, L. C. ; VELOSO, P. A. S. . Mesa Redonda: Conjuntos e Categorias. 2012. (Apresentação de Trabalho/Outra).
ENGLANDER, C. ; PEREIRA, L. C. ; HAEUSLER, E. H. . Arbitrary multi-truth-value functions and natural deduction. 2011. (Apresentação de Trabalho/Comunicação).
HAEUSLER, E. H. . Proof Theory and systems of deduction. 2011. (Apresentação de Trabalho/Conferência ou palestra).
GUEDES, L. C. C. ; HAEUSLER, E. H. . Action Algebras and Model Algebras in Denotational Semantics. 2009. (Apresentação de Trabalho/Conferência ou palestra).
Hæusler, Edward Hermann ; RUSSO, C. ; SECCO, G. . Proceedings of the XX Encontro Brasileiro de Lógica. London, 2024. (Prefácio, Pósfacio/Prefácio)>.
Hæusler, Edward Hermann ; RUSSO, C. ; SECCO, G. . Contemporary Logic in Brazil?Proceedings of the XX Encontro Brasileiro de Lógica. Berlin, 2024. (Prefácio, Pósfacio/Prefácio)>.
Carnielli, Walter ; HAEUSLER, E. H. ; VIANA, J. P. . The Proceedings of the XVII EBL?17th Brazilian Logic Conference, 2014: A preface. Oxford, UK, 2017. (Prefácio, Pósfacio/Prefácio)>.
NIEVES, J. C. ; HAEUSLER, E. H. ; VIEIRA, Bruno Lopes . Computación y Sistemas. Ciudad de Mexico, 2017. (Prefácio, Pósfacio/Prefácio)>.
HAEUSLER, E. H. ; CERRO, L. F. . Electronic Notes in Theoretical Science, n. 269. Amsterdam, 2011. (Prefácio, Pósfacio/Prefácio)>.
AYALA-RINCÓN, M. ; HAEUSLER, E. H. . Logic Journal of the IGPL 17(5), 2009. (Prefácio, Pósfacio/Prefácio)>.
AYALA-RINCÓN, M. ; HAEUSLER, E. H. . Electronic Notes in Theoretical Computer Science 205, 2008. (Prefácio, Pósfacio/Prefácio)>.
HAEUSLER, E. H. . Introdução a Teoria da Prova para Métodos Formais. Ouro Preto: SBMF 2007, 2006 (Mini-Curso ministrado em Congresso Nacional).
QUEIROZ, R. ; PEREIRA, L. C. ; HAEUSLER, E. H. . Electronic Notes in Theoretical Computer Science , n. 67, 2002. (Prefácio, Pósfacio/Prefácio)>.
HAEUSLER, E. H. ; MESEGUER, J. . MEFIA PROJECT. Brasília: CNPQ, 2001 (Coordenação de Projeto).
HAEUSLER, E. H. . Reviews of Automatic Theorem Proving by OTTER. Oxford: University of Oxford Publishing, 1996 (Review de Livro Publicado).

Outras produções

VASCONCELOS, D. R. ; Haeusler, Edward Hermann ; BENEVIDES, M. R. F. . Defining agents via strategies: Towards a view of MAS as games. 2005.

HAEUSLER, E. H. ; SCHROEDER-HEISTER, P. . Sêmantica via Teoria da Prova. 2004.

HAENDCHEN FILHO, A. ; CAMINADA, N. ; Hæusler, Edward Hermann ; STAA, A. V. . Facilitating the Specification Capture and Transformation Process in the Development of Multi-Agent Systems. 2004.

BREITMAN, K. K. ; HAENDCHEN FILHO, A. ; Haeusler, Edward Hermann . Using Ontologies to Formalize Services Specifications in Multi-Agent Systems. 2004.

HAEUSLER, E. H. ; MESEGUER, J. . Fundamentação Matemática e de Engenharia de Softwar via Arquitetura. 2000.

Haeusler, Edward Hermann ; Gordeev, L. . Proof compressions and the conjecture NP = PSPACE. 2017. (Curso de curta duração ministrado/Outra).

PAIVA, V. ; PEREIRA, L. C. ; Haeusler, Edward H. . Natural Deduction for the Working Logician. 2016. (Curso de curta duração ministrado/Outra).

HAEUSLER, E. H. . Introdução a Teoria da Prova para Métodos Formais. 2007. (Curso de curta duração ministrado/Outra).

HAEUSLER, E. H. ; OLIVEIRA, C. M. G. ; CARVALHO, R. L. . Universal Computation. 2005. (Curso de curta duração ministrado/Outra).

HAEUSLER, E. H. ; PEREIRA, L. C. . Multiplicativily Quantified Linear Logic. 1999 (Palestra) .

HAEUSLER, E. H. . Banca Concurso para Professor Adjunto UFF. 1997 (Banca de Concurso de Público) .

HAEUSLER, E. H. . Teoria das Categorias e Linguagens de Programação (8 hs) miniistrado durante o I Simpósio Brasileiro de Linguagens de Programação. 1996 (Mini-Curso Ministrado em Congresso) .

HAEUSLER, E. H. . Mini-Seminario de Teoria das Categorias em Computacao. 1996 (Mini-Curso Ministrado em Congresso) .

HAEUSLER, E. H. . Banca para Professor Assistente na área de S.I.. 1996 (Banca de Concurso de Público) .

HAEUSLER, E. H. ; MORETH, R. C. ; REYES, G. . The Decidability Of Mao. 1996 (RELATORIO TECNICO) .

HAEUSLER, E. H. . Teoria da Computacao : Uma Abordagem Semantica. 1995 (Palestra) .

HAEUSLER, E. H. . Logica Linear e Relevancia. 1995 (Palestra) .

HAEUSLER, E. H. . Ferramentas Simbolicas em IA. 1995 (Palestra) .

HAEUSLER, E. H. . Migração de Codigo : Uma Abordagem Formal. 1995 (Palestra) .

HAEUSLER, E. H. . Linear Quantifiers and Infinitary Linear Logic. 1995 (Palestra) .

HAEUSLER, E. H. . Teoria das Categorias em Computacao. 1995 (Curso de Verão Ministrado) .

HAEUSLER, E. H. . Semantica em Computacao : A abordagem Denotacional. 1995 (Curso de Verão Ministrado) .

Projetos de pesquisa

2024 - Atual

Compressão de Provas em Dedução Natural e a Questão NP=PSPACE (Bolsa PQ), Descrição: Este projeto é baseado na nossa prova, publicada em 2020, de NP=PSPACE, uma conjectura da década de 70. O artigo emquestão foi revisto por cerca de 2 anos por especialistas antes de ser publicado. A técnica usada na nossa provapertence a área de Teoria da Prova. Não é uma área bem conhecida na grande área de Ciência da Computação, e atémesmo na sub-área de Teoria da computação. O impacto do resultado e bem significativo, apesar de ainda haverresistência na aceitação do mesmo, devido ao uso destas técnicas pouco conhecidas da comunidade de CC. Desde 2020,temos trabalhado em provas mais convincentes. EM 2022, temos duas abordagens, uma não-construtiva via certificadosduplos e outra baseada em compressão de provas em grafos de prova. A primeira prova prova já está submetida a umperiodico de logica e computação. Já tivemos uma primeira interação com um dos revisores (anonima). Tem cerca de 3meses isso. No intuito de continuar meu trabalho de formação de pesquisadores, estou focando no desenvolvimento maissistemático da segunda alternativa, compressaõ de provas. Este Projeto foca no método de compressão de provasderivado desta segunda prova alternativa. Isso além de implicar na possibilidade de armazenamento de provas gigantesem forma compacta e sem a necessidade de descompactação para verificação. Feito isso, temos por objetivo a propostade desenvolvimento de uma versão em provador interativo de teoremas com provascompactas, o que implicaria em umaaceitação mais imediata pela comunidade de CC. Por exemplo, a geração de certificados sucintos para a nãohamiltonicidade de grafos também são considerados. Estes resultados mostram contribuições com indice de impactopotecialmente bem alto. Com certeza teremos muitos jovens participando dos desdobramentos desta pesquisa. Abrem-semuitas possibilidades, como por exemplo o uso de técnicas de Sat-Solvers para problemas em PSPACE. O estado da artede Sat-Solvers seria diretamente aplicável a problemas como minimização de circuitos. Estamos em uma caminho seguro,pois mesmo que os especialistas tenham deixado passar um erro essencial, já temos um método de compressão com umaprova parcialmente verificada pelo LEAN, um provador interativo de teoremas. Neste caso os casos mais comuns deprovas proposicionais de tamanho superpolinomial poderão ser compactados e verficados nesta forma, demonstrando umaaplicabilidade boa da compactação para problemas de projeto de circuitos booleanos sucintos. Em suma, mesmo que hajaalgum erro na prova de NP=PSPACE, a versão construtiva via compressão pode ser usada para o caso construtivo comNP=CoNP, também de grande impacto. E mesmo que tenha algum detalhe problematico, a compactação de provas em grafosde prova via nosso método de compressão tem uso em alguns problemas em CC que necessitam certificados negativossucintos, como certificados pequenos para a não exitência de ciclo hamiltoniano e daí minimização de circuitosbooleanos, via colapso hierarquia poly.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Lew Gordeev - Integrante / José Flávio de Barros Cavalcante - Integrante / Robinson Callou - Integrante.
2024 - Atual

Lógica e inteligibilidade de processos computacionais, Descrição: O projeto está organizado em torno de questões filosóficas eepistemológicas sobre o processamento computacional deinformações. As disciplinas mobilizadas por esse programainterdisciplinar de pesquisa são, principalmente, a Filosofia(epistemologia, filosofia da matemática, filosofia da linguagem eética), a Ciência da Computação Teórica e a Matemática. Do ponto devista científico, o projeto busca alcançar quatro objetivos:1. Desenvolver uma reflexão sobre o estatuto e a variedade delinguagens de programação.2. Investigar as consequências epistemológicas do uso docomputador nas ciências, inclusive na matemática, como umaferramenta adicional para a produção de evidências.3. Apresentar e analisar criticamente as abordagens computacionaiscontemporâneas para a questão dos fundamentos da matemática epara a noção de tipo;4. Explorar os desafios epistemológicos oriundos da evolução recenteda teoria matemática da computabilidade e da complexidadecomputacional. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (1) / Doutorado: (5) . , Integrantes: Edward Hermann Haeusler - Integrante / Luiz Carlos Pereira - Coordenador / Wagner Sanz - Integrante / Jean Baptiste Joinet - Integrante / Gilles Dowek - Integrante / Bruno Lopes Vieira - Integrante / Abel Lassalle Casanave - Integrante., Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro.
2023 - Atual

Neurorobótica educacional: uma proposta de inclusão de crianças com severas deficiências motoras na Robótica. NEUROASSIST, Descrição: O uso de robótica emambientes educacionais vem se tornando cada vez mais presente no ensino de crianças,aumentando muito o engajamento delas no aprendizado de conteúdo curriculares formais. O nossoconhecimento da fisiologia do sistema nervoso conta com enormes avanços recentes, incluindo ahabilidade de treinar pessoas no controle da atividade elétrica em regiões arbitrárias do córtexcerebral, uma técnica denominada neurofeedback. Este projeto tem o objetivo treinar crianças comseveras dificuldades de movimento, utilizando a técnica de neurofeedback em uma interfacecérebro-máquina, de maneira que estas possam participar de processos de ensino-aprendizagemenvolvendo a expressão de seu movimento, particularmente em processos de ensino-aprendizagem mediados pela robótica educacional. Assim, esperamos habilitar a comunicação daintenção dos seus movimentos em uma plataforma de aprendizagem baseada em robóticaeducacional, ampliando as possibilidades de seu percurso de aprendizagem e de sua inclusão social. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (6) / Especialização: (2) / Mestrado acadêmico: (3) / Doutorado: (7) . , Integrantes: Edward Hermann Haeusler - Integrante / José Valentim dos Santos Filho - Integrante / Pedro Valadão Carelli - Integrante / Aquiles Medeiros Filgueira Burlamaqui - Integrante / Nivaldo Antonio Portela de Vasocncelos - Coordenador.
2023 - Atual

CiberSemântica, Descrição: O Projeto Ciber Semântica foi concebido para ser uma aplicação de Inteligência Artificial para odomínio cibernético, atuando no nível semântico. Para tanto é necessário muito esforço de pesquisa emTeoria da Computação, uma vez que a modelagem e o processamento de conhecimento vai depender demodelos de lógica que permitam inferências e verificação de hipóteses.A Inteligência Artifical entra na automação do levantamento de hipóteses, denominadas insights,com base em interesses da Defesa Cibernética. Esse processo acontece de forma criativa para o serhumano, o que leva tempo e esforço variáveis. A automação de insights permite acelerar o processo deAnálise Cibernética e aumentar sua qualidade também.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Especialização: (3) / Mestrado acadêmico: (3) / Doutorado: (5) . , Integrantes: Edward Hermann Haeusler - Integrante / Ricardo Queiroz de Araujo Fernandes - Coordenador / Bernardo Alkmin - Integrante / Robinson Callou - Integrante / Bruno Cuconato - Integrante / Anderson Silva - Integrante., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2021 - 2024

Aplicabilidade de nova tecnologia voltada para o desenvolvimento de um modelo de monitoramento inteligente dos ativos de transmissão, Descrição: Projeto de PD ANEEL, obtido por chamada publica em 2018.INicio em 2021. 3 anos de duração.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Especialização: (3) / Mestrado acadêmico: (2) / Doutorado: (3) . , Integrantes: Edward Hermann Haeusler - Coordenador / Alex Vasconcelos Garcia - Integrante / Jefferson Santos - Integrante / Pedro Schneider - Integrante / Carla Chrystina de Castro - Integrante / Cláudio dos Santos Pereira - Integrante / Gabriel Resende Machado - Integrante / Edmilson Siqueira Varejão Neto - Integrante / Renato Santos de Jesus - Integrante / Gabriela Queyroi Chaves - Integrante., Financiador(es): Centrais Elétricas - Sede - Cooperação.
2019 - 2022

SMO - Desenvolvimento e aperfeiçoamento de sistemas de apoio as operações offshore (ANP-Petrobras), Descrição: P D Petrobras Project ANP funding. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (4) / Mestrado acadêmico: (1) / Mestrado profissional: (1) / Doutorado: (0) . , Integrantes: Edward Hermann Haeusler - Coordenador / DE BARROS SANTOS, JEFFERSON - Integrante., Financiador(es): Agência Nacional do Petróleo - Auxílio financeiro.
2019 - Atual

Compressão de provas e a conjectura NP = PSPACE (APQ1-Faperj), Descrição: Projeto de pesquisa modalidade APQ1 - Auxílio da pesquisa básica - FAPERJResumo - A Teoria da Prova, iniciada por Hilbert, tem se mostrado uma ferramenta teórica e de fundamentacão de amplo espectro em ciência da computação. Suas contribuições aparecem em áreas desde complexidade computacional a engenharia de software e representação do conhecimento. Por exemplo, algumas de suas mais relevantes contribuições envolvem geração de programas a partir de provas intuicionistas, semântica de programas e sistemas de computação, via diversos sistemas de tipo e ?-calculi e finalmente otimização de có digo funcional via combinadores. Teoria da prova também é fortemente utilizada como fundamento para formalismos de especificação e validação de teorias na matemática construtiva. Este projeto propõe o estudo de uma abordagem baseada em teoria da prova em ciência da computação, abordando, em específico, o tema de produção de provas curtas (compressão de provas), bem como de seu uso no auxílio a processos de validação de bases de conhecimento em domínios específicos. Como é bem sabido, a existência de provas curtas (de tamanho polinomial em relação a conclusão da prova) para todas as tautologias de uma lógica proposicional L implica em NP = PSPACE, se L é a lógica minimal ou a lógica intuicionista e CoNP = NP se a L e a lógica clássica. Particularmente, se NP = PSPACE então CoNP = NP... , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Especialização: (0) / Mestrado acadêmico: (3) / Mestrado profissional: (2) / Doutorado: (4) . , Integrantes: Edward Hermann Haeusler - Coordenador / Alex Vasconcelos Garcia - Integrante / Mario Roberto Folhadela Benevides - Integrante / Luiz Carlos Pereira - Integrante / Bruno Lopes Vieira - Integrante / Cecilia Lustosa - Integrante / DE BARROS SANTOS, JEFFERSON - Integrante., Financiador(es): FAPERJ - Auxílio financeiro.
2014 - 2018

MCTI/CNPQ/Universal 14/2014 - Faixa B, Descrição: A Teoria das Categorias tem um estreito relacionamento com modelos de semântica para computação e sistemas computacionais, assim como uma forte ligação com a teoria da prova através da semântica para sistemas lógicos via extensões do isomorfismo Curry-Howard. Este projeto de pesquisa investiga como a Teoria da Prova e a Teoria das Categorias podem contribuir como base teórica para a fundamentação de Linguagens e Abordagens Lógicas e Semânticas. OBJETIVO Os objetivos principais deste projeto são: (i) Investigar como técnicas e ferramentas da Teoria das Categorias podem ser usadas no processo de especificação semântica de modelos e sistemas (ii) Investigar como o uso de conceitos, técnicas e abordagens em Teoria da Prova podem ser usados na fundamentação de Linguagens e abordagens lógicas para a representação de conhecimento e modelos de sistemas (provavvelmente com o uso de Ontologias Formais) (iii) Relacionar os ítens i e ii acima através de morfismos composicionais (Funtores) e associar uma semântica computável a estes morfismos.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) / Doutorado: (4) . , Integrantes: Edward Hermann Haeusler - Coordenador / Isabel Leite Cafezeiro - Integrante / Christiano de Oliveira Braga - Integrante / Geiza Maria Hamazaki da Silva - Integrante / Mario Roberto Folhadela Benevides - Integrante / Alexandre Rademaker - Integrante / Lew Gordeev - Integrante / Luiz Carlos Pereira - Integrante / Vaston Gonçalves Costa - Integrante / Jean Baptiste Joinet - Integrante / Gilles Dowek - Integrante / Marcela Quispe Cruz - Integrante / Jefferson Santos - Integrante / Hugo Macedo - Integrante / Bruno Lopes Vieira - Integrante / Cecilia Lustosa - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
2014 - 2018

Login- Logic and Information - STIC-AmSUD, Descrição: Cooperação entre PUC-Rio, Universidade de Buenos Aires e INRIA no desenvolvimento de ferramentas e lógicas para o suporte ao projeto e validação de sistemas e modelos computacionais. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Edward Hermann Haeusler - Coordenador / Luiz Carlos Pereira - Integrante / Jean Baptiste Joinet - Integrante / Gilles Dowek - Integrante / Marcela Quispe Cruz - Integrante / Jefferson Santos - Integrante / Bruno Lopes Vieira - Integrante / Cecilia Lustosa - Integrante / Ricardo Oscar - Integrante.
2014 - 2017

Certificação de software através de Lógica Dinâmica e Redes de Petri (Edital 29/2014 FAPERJ), Descrição: Lógica Proposicional Dinâmica (PDL) e ́ um sistema lógico multi-modal utilizada para especificar e verificar propriedades em programas sequenciais. Redes de Petri são um formalismo largamente utilizado na especificação de sistemas concorrentes e possuem uma interpretação/apelo gráfica bastante intuitiva. Neste trabalho apresentam-se aplicações de extensões da Lógica Proposicional Dina?mica onde os programas sa ̃o substituídos por Redes de Petri Estoca ́sticas de forma a efetuar a verificação formal de propriedades em software. O objetivo e ́ converter automaticamente especificações UML em Redes de Petri Estocásticas para efetuar inferências e validar propriedades, certificando o sistema.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Edward Hermann Haeusler - Coordenador / Christiano de Oliveira Braga - Integrante / Mario Roberto Folhadela Benevides - Integrante / Vaston Gonçalves Costa - Integrante / Gilles Dowek - Integrante / Cláudia Nalon - Integrante / Bruno Lopes Vieira - Integrante., Financiador(es): FAPERJ - Auxílio financeiro.
2014 - 2016

BJT- Bolsa Jovens Talentos (Dr. Hugo Daniel dos Santos Macedo, Descrição: Bolsa de pesquisa de 3 anos para o Dr. Hugo Macedo realizar trabalho de pesquisa no ambito de Teoria das Categorias em sistemas computacionais e modelos.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Jefferson Santos - Integrante / Hugo Macedo - Integrante / Bruno Lopes Vieira - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.
2013 - 2017

GetFun - Generalizing truth-functionality, Descrição: A coordinated exchange programme for the investigation of compositional meaning in logic and applications. The scientific guideline of the GeTFun project is to study and relate various well-motivated ways in which the attractive properties and meta-properties of truth-functionality may be generalized to cover more extensive logical grounds. Besides the abstract, model- and proof-theoretical aspects, the project will keep a strong focus in meaningful application areas where the complexity of the phenomena involved goes beyond the scope of standard approaches. The impact and relevance of the proposed line of work should accordingly be measured directly by its foundational character with respect to a better and deeper understanding of meaning in logics modeling complex phenomena and, of necessity, suitable general forms of compositional reasoning.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (3) . , Integrantes: Edward Hermann Haeusler - Integrante / Alexandre Rademaker - Integrante / Luiz Carlos Pereira - Integrante / João Marcos Almeida - Integrante / Rajsvan Diaconescu - Integrante / Jean Yves Beziau - Integrante / Carlos Caleiro - Coordenador / Ofer Arieli - Integrante / Arnon Avron - Integrante / Carolina Blasio - Integrante / Ori Lahav - Integrante / Yaroslav Shramko - Integrante / Luca Viganò - Integrante., Financiador(es): Research Executive Agency - Cooperação.
2012 - 2013

Universal 14/2011 - Lógica intuicionista como base para ontologias jurídicas, Descrição: Este projeto visa investigar a efici?encia da l ́ogica descritiva intuicionista como alternativa `a ALC cl ́assica, com foco no dom ́ınio das ontologias jur ́ıdicas. Assim, espera-se promover a consolida ̧ca ̃o de conhecimentos de teoria da prova, focado na prova automa ́tica de teoremas. Al ́em dos estudos sobre l ́ogica descritiva, propo ̃e-se o desenvolvimento de um ferramental para a prova automa ́tica de teoremas atrav ́es de tableaux e dedu ̧ca ̃o natural. Esse mesmo ferramental ser ́a adequado de forma que possa ser utilizado no ensino de l ́ogica em cursos de graduac ̧a ̃o e po ́s-gradua ̧ca ̃o. Por fim, trabalhar-se- ́a num m ́odulo do provador para explicac ̧a ̃o em termos jur ́ıdicos.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) / Doutorado: (3) . , Integrantes: Edward Hermann Haeusler - Coordenador / Valeria de Paiva - Integrante / Mario Roberto Folhadela Benevides - Integrante / Alexandre Rademaker - Integrante / Luiz Carlos Pereira - Integrante / Cecília Englander - Integrante / Bruno Lopes Vieira - Integrante / V. Pinheiro - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa., Número de produções C, T & A: 6
2010 - 2013

Théories contemporaines de la logique et philosophie du langage : enjeux épistémologiques et sémantiques, Projeto certificado pelo(a) coordenador(a) Luiz Carlos Pinheiro Dias Pereira em 07/03/2018., Descrição: Estudos lógicos e filosóficos da linguagem. Ênfase em semântica baseada em Teoria da prova. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (4) . , Integrantes: Edward Hermann Haeusler - Integrante / Paulo Augusto Silva Veloso - Integrante / Luiz Carlos Pereira - Coordenador / Cecília Englander - Integrante / Bruno Lopes Vieira - Integrante / Jean Baptiste Joinet - Integrante / Gilles Dowek - Integrante., Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro., Número de produções C, T & A: 4
2009 - 2012

Projeto e Desenvolvimento de Redes de Sensores sem Fios, Descrição: Estudo, pesquisa e desenvolvimento de técnicas e métodos para a implementação e validação formal de redes de sensores.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (4) / Mestrado acadêmico: (1) / Mestrado profissional: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Integrante / Eliana da Silva Almeida - Integrante / Bruno Lopes Vieira - Integrante / Ajejandro Frey - Coordenador / Antonio Loureiro - Integrante., Financiador(es): CAPES - Centro Anhanguera de Promoção e Educação Social - Auxílio financeiro.
2009 - 2011

Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Este projeto trata do uso de técnicas conjugadas de reconhecimento de padrão (processamento de sinais) e ontologias (lógica de Descrição), bem como da modelagem (ontologias) de simulações e ensaios em escala de plataformas de petróleo, para a recuperação de informação/conhecimento (Knowledge Mining) via "queries" lógicas. O projeto forneceu ao CENPES/Petrobrás um set bem amplo de suas simulações e ensaios que estavam em estado de material legado. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / V. Pinheiro - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro.
2005 - 2007

(CTINFO) Anubis: Um Framework para Análise Formal de Sistemas Multi-Agente para Segurança da Informação, Descrição: Modelagem e Análise de Sistemas Multi-Agentes com camada de Segurança (Trust). , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (4) . , Integrantes: Edward Hermann Haeusler - Coordenador / Isabel Leite Cafezeiro - Integrante / Carlos José Pereira de Lucena - Integrante / Christiano de Oliveira Braga - Integrante / Geiza Maria Hamazaki da Silva - Integrante / Fernando Naufel do Amaral - Integrante / Markus Endler - Integrante / Davi Romero Vasconcelos - Integrante / Juliana Carpes Imperial - Integrante / Mario Roberto Folhadela Benevides - Integrante / Alexandre Rademaker - Integrante / Carlos Bazílio Martins - Integrante / Vaston Gonçalves Costa - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / MODULO SECURITY S.A. - Cooperação., Número de produções C, T & A: 20
2005 - 2006

Teoria da Prova na Fundamentação do Processo de Teoria da Prova na Fundamentação do Processo de Especificação e Validação de Sistemas, Descrição: A presente proposta tem por objetivos a justificação de uma abordagem baseada em teoria da prova para a fundamentação do processo de desenvolvimento e validação de software. Dentro deste escopo tem-se os seguintes objetivos espeçificos: 1- Justificação da abordagem baseda no Isomorfismo Curry-Howard com uso de especificação abstrata de dados e funcionalidades em lógica poli-sortida de primeira ordem, em detrimento da abordagem totalmente construtiva baseada em lógica de alta ordem e teoria intuicionista dos tipos. \item Aprimoramento dos sistemas de Dedução Natural para lógicas de tempo ramificado com uso em análise formal de especificação de sistemas reativos. Trata-se neste caso do aprimoramento de dos sistemas para CTL e CTL* e seu uso em especificação. A abordagem geral para quantificação em Dedução Natural é um resultado em lógica bastante interessante neste ponto, apesar de não estar diretamente conectado com a ciência da computação. 2- Desenvolvimento de critérios de identidade para provas que se mostrem mais adequados no tocante à interpretação, em teoria das categorias, do isomorfismo Curry-Howard. Este tópico está bastante inserido no projeto CAPES-DAAD coordenado pelo autor. 3- Conclusão do trabalho em interoperabilidade formal, com o desenvolvimento da sua contra-partida em teoria da prova. 4- Implementação dos modelos propostos em [Fnaufel] na forma de Framework (software) com análise formal provida por prova de teoremas em Teoria Local dos Conjuntos. Desenvolvimento de alguma ferramenta para o suporte, ao menos semi-automático, a prova de teoremas em Teoria Local dos Conjuntos. 4- Desenvolvimento de sistemas dedutivos para a lógica modal de jogos e definição de um verificador de modelos para a mesma (tarefas independentes). O uso da técnica utilizada em [Renteria & Haeusler] será explorada por Davi Romero (aluno de doutorado) neste contexto. Pesquisa preliminar em lógica modal foi publicada em [MAS e Jogos] pela equipe do autor.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (2) Doutorado: (3) . , Integrantes: Edward Hermann Haeusler - Coordenador / Isabel Leite Cafezeiro - Integrante / Christiano de Oliveira Braga - Integrante / Geiza Maria Hamazaki da Silva - Integrante / Christian Jacques Renteria - Integrante / Fernando Naufel do Amaral - Integrante / Alfio Martini - Integrante / Uwe Wolter - Integrante / Juliana Vizzoto - Integrante / Davi Romero Vasconcelos - Integrante / Juliana Carpes Imperial - Integrante / Mario Roberto Folhadela Benevides - Integrante / Alexandre Rademaker - Integrante / Luiz Carlos Pereira - Integrante / Carlos Bazílio Martins - Integrante., Financiador(es): Fundação Carlos Chagas Filho de Amparo à Pesquisa do Estado do RJ - Auxílio financeiro., Número de produções C, T & A: 27
2004 - 2006

Semântica via Teoria da Prova, Descrição: Projeto de Cooperação CAPES-DAAD. Objetiva o uso de Teoria da Prova para atribuir semântica à sistemas computacioanais , modelos e construções linguísticas.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (3) . , Integrantes: Edward Hermann Haeusler - Coordenador / Marcelo da Silva Corrêa - Integrante / Christian Jacques Renteria - Integrante / Davi Romero Vasconcelos - Integrante / Peter Schroeder-Heister - Integrante / Lew Gordeev - Integrante / Luiz Carlos Pereira - Integrante / Vaston Gonçalves Costa - Integrante / Wagner Sanz - Integrante., Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro / Deutscher Akademischer Austauschdienst - Auxílio financeiro., Número de produções C, T & A: 23
2000 - 2002

MEFIA : Mathematical and Engeneering Foundations for Interoperability via Architecture (CNPQ-NSF), Descrição: Os objetivos deste projeto são: (1) O desenvolvimento de fundamentos matemáticos para integrar e interoperar de forma coerente e rigorosa diversos componentes, de sistemas orientados a objetos distribuídos, tais como : descrições de arquitetura, especificações formais e protótipos executáveis. (2) Baseando-se em tais fundamentos, desenvolver uma metodologia para o projeto, desenvolvimento e evolução de sistemas que suporte uma integração transparente de descrições informais e formais de sistemas e torne explícito as restrições que as diferentes visões que os componentes se impõem mutuamente. O desenvolvimento da fundamentação matemática terá seu início com o estudo de uma ampla gama de notações e formalismos, dentre aqueles que se mostram promissores a descrição de sistemas em diferentes níveis, e seus relacionamentos mútuos. Dentre estes estão incluídos modelos semânticos para concorrência e interação, lógicas de especificação de alta ordem, notação de projeto, cálculo de objetos e linguagens de especificação executáveis. Lógica de Reescrita desempenhará um papel importante não só como formalismo executável, mas também como abordagem metalógica reflexiva na qual os formalismos escolhidos e seus relacionamentos serão especificados. Estas especificações serão executadas nas meta-ferramentas desenvolvidas em Maude (uma implementação de lógica de reescrita). O desenvolvimento de uma metodologia baseada nos fundamentos propostos será guiada por estudos de caso nos quais o conjunto de formalismos e seus relacionamentos sistemáticos serão aplicados e testados em aplicações concretas que demonstrem a interoperação dos formalismos e seus benefícios. É esperado que tais fundamentos e metodologia contribuam para o avanço do estado-da-arte em desenvolvimento e evolução de Software, e, indiquem novas ferramentas e métodos que, quando usados de forma apropriada, reduzirão o custo e e esforço na manutenção e desenvolvimento de Sofwtare.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (3) Doutorado: (3) . , Integrantes: Edward Hermann Haeusler - Coordenador / Alex Vasconcelos Garcia - Integrante / Armando Haerberer - Integrante / Tom Maibaum - Integrante / José Luiz Lopes Fiadeiro - Integrante / José Meseguer - Integrante / Peter D Mosses - Integrante / Alfio Martini - Integrante / Paulo Blauth Menezes - Integrante / Carolyn Talcott - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / National Science Foundation - Cooperação., Número de produções C, T & A: 33
1994 - 1998

PRATICA (PRovAs, TIpos e CAtegorias), Descrição: Modelagem dos aspectos categoricos e algebricos dos diversos Lambda-calculi. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (3) . , Integrantes: Edward Hermann Haeusler - Coordenador / Marcelo da Silva Corrêa - Integrante / Valeria de Paiva - Integrante / Regina Celia Moreth - Integrante / Luiz Carlos Pereira - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 18

Projetos de desenvolvimento

2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante.Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador.Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.
2007 - 2010

(DMH) Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos, Descrição: Modelagem e Desenvolvimento de ferramentas para armazenamento e recuperação de Modelos Hidrodinâmicos. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) / Doutorado: (1) . , Integrantes: Edward Hermann Haeusler - Coordenador / Geiza Maria Hamazaki da Silva - Integrante / Alexandre Rademaker - Integrante., Financiador(es): Petróleo Brasileiro - Rio de Janeiro - Matriz - Auxílio financeiro., Número de produções C, T & A: 2
2000 - 2001

(CTPETRO) GRECO : Gerador de Relatórios Reconfigurável, Descrição: O projeto objetiva desenvolver uma nova solução para o problema da emissão de relatórios do atual sistema Petrox. O Petrox é um simulador de processos químicos, desenvolvido pelo CENPES para uso interno à Petrobrás. Ele vem sendo desenvolvido ao longo de mais de uma década, e é constituído de um núcleo básico de cálculo, uma interface para entrada de dados, e um gerador de relatórios. O programa foi inicialmente desenvolvido exclusivamente em Fortran para um computador de grande porte, mas atualmente vem sofrendo modificações com o intuito de facilitar a manutenção e o desenvolvimento de novos módulos. Um protótipo de interface gráfica em C++ foi construído e uma versão operacional está em fase de testes. Também alguns trechos do núcleo de cálculo foram modificados, utilizando rotinas em C. O gerador de relatórios atual é um dos módulos mais antigos. O formato e conteúdo dos relatórios é fixo e está codificado diretamente em Fortran, tornando sua manutenção penosa e custosa. Com o aumento do número de usuários nos diversos órgãos da Companhia, criou-se também uma demanda por relatórios personalizados, cujo custo de implementação é inviável na atual arquitetura. Com o intuito de alavancar a adoção do Petrox em todos os setores da Petrobrás, o SEPROJ decidiu então, junto com o projeto da interface gráfica, reformular a geração de relatórios do simulador. Especificações: 1. Gerador de relatórios consistirá de um módulo executável independente da interface gráfica e do núcleo de simulação principal 2. Sistema deverá executar no mínimo nas seguintes plataformas: Windows 95/98/NT e Linux. 3. Módulo poderá ser executado diretamente, via linha de comando, ou de dentro de outro aplicativo, usando uma chamada ao sistema. 4. Os parâmetros necessários à geração do relatório devem ser todos indicados na linha de comando, usando arquivos de configuração editáveis pelo desenvolvedor ou pelo usuário. 5. Não deve haver restrições quando à localização dos arquivos de configuração e d. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Edward Hermann Haeusler - Coordenador., Financiador(es): Financiadora de Estudos e Projetos - Auxílio financeiro.

Prêmios

2023

Best paper no XVI Conferência Brasileira de Inteligência Computacional, Sociedade de Inteligência Computacional.

2020

Best paper do International Workshop on Conceptual Modeling for Life Sciences (CMLS) - 39th International Conference on Conceptual Modeling., ER2020.

2018

Menção Honrosa SBBD 2018 Demos - um dos 3 melhores trabalhos, SBC., SBC.

2017

Pesquisador Homenageado, Simpósio Brasileiro de Métodos Formais da SBC - Sociedade Brasileira de Computação., Sociedade Brasileira da Computação, SBC.

2016

Professor homenageado da turma de Bacharelado em Ciência da Computação 2016.2, PUC-Rio.

2015

Paraninfo da turma de Bacharelado em Ciência da Computação 2015.2, PUC-Rio.

2014

Professor homenageado da turma de Bacharelado em Ciência da Computação 2014.2, PUC-Rio.

2013

Paraninfo da turma de Bacharelado em Ciência da Computação 2013.1, PUC-Rio.

2012

Festschirifft at LSFA 2012 International conference. Celebration's Volume in http://www2.ic.uff.br/~cbraga/hermann50/hermann50.pdf, Workshop in Logical Frameworks with Applications. http://www2.ic.uff.br/~cbraga/hermann50/.

2005

Cientistas do Nosso Estado, FAPERJ.

2001

BEST PAPER AWARD, CHAOS - Belgium (Symposium on Computer Science, Algorithms and Programs (CASYS'2001).

2001

Paraninfo da turma de Engenharia de Computação 2001.2, PUC-Rio.

1990

Patrono da turma de Bacharelado em Ciência da Computação da UFF, 1990.1, UFF.

Histórico profissional

Endereço profissional

Pontifícia Universidade Católica do Rio de Janeiro, Centro Técnico-Científico, Departamento de Informática. , Rua Marquês de São Vicente, 225, Gávea, 22453-900 - Rio de Janeiro, RJ - Brasil, Telefone: (21) 35299385, Fax: (21) 35115645

Experiência profissional

2024 - Atual

Universidade do Estado do Rio de Janeiro

Vínculo: , Enquadramento Funcional:

2023 - Atual

Universidade Federal de Pernambuco

Vínculo: , Enquadramento Funcional:

2023 - Atual

Fundação de Apoio à Pesquisa,Desenvolvimento e Inovação-Exercito Brasileiro

Vínculo: , Enquadramento Funcional:

2008 - Atual

Sociedade Brasileira de Lógica

Vínculo: Colaborator, Enquadramento Funcional: Primeiro Vice-Presidente

1991 - Atual

Pontifícia Universidade Católica do Rio de Janeiro, PUC-Rio

Vínculo: Servidor público ou celetista, Enquadramento Funcional: PROFESSOR ASSOCIADO, Carga horária: 44

1985 - 1986

Pontifícia Universidade Católica do Rio de Janeiro, PUC-Rio

Vínculo: Servidor público ou celetista, Enquadramento Funcional: INSTRUTOR HORISTA, Carga horária: 8

Atividades

11/2001
Direção e administração, Centro Técnico-Científico, Departamento de Informática.,Cargo ou função, Membro Titular da Comissão de Pós-Graduação do Departamento de Informática.
03/2000
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/1999
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/1996
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/1996
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
08/1992
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/1991
Ensino, Informática, Nível: Pós-Graduação,Disciplinas ministradas, Lógica e Especificação, Computabilidade, Semântica de Linguagens, Teoria das Categorias, Lógica Modal e Temporal, Teoria de Topos I, Teoria de Topos II, Teoria Intuicionista dos Tipos
03/1991
Ensino,,Disciplinas ministradas, ICC, Lógica e Especificação, Computabilidade, Semântica de Linguagens de Programação, Teoria da Programação, Linguagens Formais e Autômatos, Estruturas Discretas, Linguagens de Programação I, Introdução a Engenharia
09/2001 - 10/2001
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
07/2001 - 07/2001
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/2000 - 07/2001
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/2001 - 06/2001
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
08/1998 - 04/2001
Direção e administração, Centro Técnico-Científico, Departamento de Informática.,Cargo ou função, Coordenador de Graduação do Departamento de Informática.
03/1999 - 03/2001
Extensão universitária , Centro Técnico-Científico, Departamento de Informática.,Atividade de extensão realizada, Professor do Curso de Especialização em Redes.
03/2000 - 12/2000
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
10/1997 - 10/1999
Direção e administração, Centro Técnico-Científico, Departamento de Informática.,Cargo ou função, Membro Titular da Comissão de Pós-Graduação do Depto de Informática.
05/1999 - 05/1999
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/1994 - 12/1998
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/1994 - 12/1996
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
01/1996 - 02/1996
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
10/1993 - 12/1995
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
03/1993 - 03/1995
Direção e administração, Centro Técnico-Científico, Departamento de Informática.,Cargo ou função, Coordenador de Graduação do Depto de Informática.
05/1994 - 08/1994
Pesquisa e desenvolvimento, Centro Técnico-Científico, Departamento de Informática.,Linhas de pesquisa
10/1992 - 10/1993
Direção e administração, Centro Técnico-Científico, Departamento de Informática.,Cargo ou função, Membro Titular da Comissão de Pós-Graduação do Depto de Informática.

1991 - 1991

Universidade Federal Fluminense

Vínculo: Servidor público ou celetista, Enquadramento Funcional: Professor Adjunto, Carga horária: 40

1991 - 1991

Universidade Federal Fluminense

Vínculo: Servidor público ou celetista, Enquadramento Funcional: Professor Adjunto, Carga horária: 40

1991 - 1991

Universidade Federal Fluminense

Vínculo: Servidor público ou celetista, Enquadramento Funcional: Professor Adjunto I, Carga horária: 40

1989 - 1990

Universidade Federal Fluminense

Vínculo: Servidor público ou celetista, Enquadramento Funcional: Professor Assistente, Carga horária: 40

1989 - 1990

Universidade Federal Fluminense

Vínculo: Servidor público ou celetista, Enquadramento Funcional: Professor Assistente, Carga horária: 40

1986 - 1989

Universidade Federal Fluminense

Vínculo: Professor Visitante, Enquadramento Funcional: Professor Assistente, Carga horária: 40

Atividades

12/1989 - 09/1991
Direção e administração, Centro de Estudos Gerais, Departamento de Computação.,Cargo ou função, COORDENACAO DE PESQUISA. COORDENACAO DE PESQUISA..
08/1986 - 08/1991
Pesquisa e desenvolvimento, Centro de Estudos Gerais, Departamento de Computação.,Linhas de pesquisa
08/1986 - 08/1991
Ensino,,Disciplinas ministradas, ASPECTOS FORMAIS DA COMPUTACAO I E II; SISTEMAS FORMAIS.

1985 - 1986

Universidade Estácio de Sá

Vínculo: Servidor público ou celetista, Enquadramento Funcional: PROFESSOR ASSISTENTE, Carga horária: 8

Outras informações:
Ensino de Fortran e Estruturas de Dados

Atividades

03/1985 - 07/1986
Ensino,,Disciplinas ministradas, Fortran, Estruturas de Dados