pubs.bib

@INPROCEEDINGS{do06:_ontol_approac_formal_infor_secur_polic,
	url = {https://ieeexplore.ieee.org/document/4031261},
	timestamp = {2023-08-07 18:59:16 (-03)},
	author = {Fernando Naufel do Amaral and C. Bazilio and G.M.H. da Silva and A. Rademaker and E.H. Haeusler},
	booktitle = {2006 10th IEEE International Enterprise Distributed Object Computing Conference Workshops (EDOCW'06)},
	title = {An Ontology-based Approach to the Formalization of Information Security Policies},
	year = {2006},
	volume = {},
	number = {},
	doi = {10.1109/EDOCW.2006.21}
}

@inproceedings{fnaufelAow07,
	address = {Gold Coast, Queensland, Australia},
	abstract = {We present the structure of an ontology for Information Security (IS), applied to the extraction of knowledge from Natural Language texts (IS standards, security policies and security control descriptions). This ontology is composed of the vocabulary for the IS Domain, and a particular kind of ontology description, logical forms to determine the structure of the DL formulas associated with the texts.  We also discuss the relationship between the structure of the formulas and the efficiency of the reasoner.},
	author = {G.M.H. da Silva and A. Rademaker and D.R. Vasconcelos and Fernando Náufel do Amaral and C. Bazílio and V. Gonçalves and E.H. Haeusler},
	booktitle = {AOW -- The Third Australasian Ontology Workshop},
	title = {Dealing with the Formal Analysis of Information Security Policies through Ontologies: A Case Study},
	year = {2007}
}

@article{fnaufelBsl00,
	address = {Lodz, Poland},
	url = {https://fnaufel.github.io/publications/fnaufel-bsl-00.pdf},
	abstract = {This paper defines an action logic featuring an operator that denotes necessary conditions,  postconditions, and time bounds of actions in a timed computational transition system. Weak completeness of an axiomatization for the logic is proved.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	journal = {Bulletin of the Section of Logic (Lodz, Poland)},
	number = {4},
	pages = {151--160},
	title = {Completeness of an Action Logic for Timed Transition Systems},
	volume = {29},
	year = {2000}
}

@Thesis{fnaufelDissert00,
	annotation = {Dissertação de Mestrado.},
	url = {https://fnaufel.github.io/publications/fnaufel-dissert-00.pdf},
	address = {Rio de Janeiro},
	abstract = {This dissertation defines RETOOL, an action logic featuring an operator to denote necessary conditions and postconditions of actions in a timed transition system (an extension of the formalism of transition systems meant to model real-time reactive/concurrent computational systems). A semantics for RETOOL is presented and compared to previous proposals. An adequate axiomatization is given, along with detailed correctness and weak completeness proofs.},
	author = {Fernando Náufel do Amaral},
	school = {Depto. de Informática, PUC-Rio},
	title = {RETOOL: uma Lógica de Ações para Sistemas de Transição Temporizados},
	year = {2000}
}

@inproceedings{fnaufelDl2008,
	url = {https://fnaufel.github.io/publications/fnaufel-dl-2008.pdf},
	address = {Dresden, Germany},
	abstract = {Many visualization frameworks for ontologies in general and for concept expressions in particular are too faithful to the syntax of the languages in which those objects are represented (e.g., RDF, OWL, DL). Model outlines depart from this tradition in that they consist of diagrams characterizing the class of models of a given concept expression. We hope this semantically-oriented visualization strategy will allow users to obtain deeper insights about the meaning of such expressions, thereby preventing errors of design or of interpretation.},
	author = {Fernando Náufel do Amaral and C. Bazílio},
	booktitle = {The 21st International Workshop on Description Logics},
	title = {Visualization of Description Logic Models},
	year = {2008}
}

@inproceedings{fnaufelEbl06,
	url = {https://fnaufel.github.io/publications/fnaufel-ebl-06.pdf},
	address = {Itatiaia, Rio de Janeiro},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	booktitle = {XIV EBL -- Encontro Brasileiro de Lógica},
	title = {Using the Internal Logic of a Topos Related to the Topos of Forests to Model Search Spaces for Problems},
	year = {2006}
}

@Report{fnaufelFaperj96,
	address = {Rio de Janeiro},
	author = {Fernando Náufel do Amaral},
	institution = {FAPERJ},
	number = {E-26/151.163/95-BOLSA},
	title = {Uma Nova Proposta para o Cálculo do Fecho Transitivo de Relações Binárias},
	year = {1996}
}

@article{fnaufelIgpl07,
	url = {https://fnaufel.github.io/publications/fnaufel-igpl-07.pdf},
	abstract = {We present a structural model for (meta)heuristic search strategies for solving computational problems. The model is defined through the use of topos-theoretical tools and techniques which provide an appropriate internal logic (with the language of local set theory) where objects of interest can be represented.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	journal = {Logic Journal of the IGPL},
	number = {5--6},
	pages = {457--474},
	title = {Using the Internal Logic of a Topos to Model Search Spaces for Problems},
	volume = {15},
	year = {2007}
}

@InProceedings{fnaufelJaiio99,
	address = {Buenos Aires, Argentina},
	url = {https://fnaufel.github.io/publications/fnaufel-jaiio-99.pdf},
	abstract = {Well-integrated development tools, allowing automatic code generation from visual representations of analysis and design decisions, are important assets in handling the complexities of today's software. This paper describes several message passing semantics for the expression of concurrency in a new object-oriented visual development system, along with the C$^++$ idioms generated for asynchronous messages.},
	author = {Fernando Náufel do Amaral and P.G. Rabelo and S.E.R. Carvalho},
	booktitle = {28 JAIIO -- Jornadas Argentinas de Informática e Investigación Operativa},
	title = {C++ Idioms for Concurrent Operations},
	year = {1999}
}

@inproceedings{fnaufelLaptec02,
	url = {https://fnaufel.github.io/publications/fnaufel-laptec-02.pdf},
	address = {São Paulo, São Paulo},
	abstract = {A specification language for real-time software systems is presented. Notions from Category Theory are used to specify how the components of a system should interact. The potential role of the proposed language in the search for interoperability of specification formalisms is briefly discussed.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler and M. Endler},
	booktitle = {Advances in Logic, Artificial Intelligence {and} Robotics -- LAPTEC 2002},
	editor = {J.M. Abe and J.I. da Silva Filho},
	pages = {194--201},
	publisher = {IOS Press},
	series = {Frontiers {in} Artificial Intelligence {and} Applications},
	title = {A Real-Time Specification Language},
	volume = {85},
	year = {2002}
}

@inproceedings{fnaufelLc00,
	url = {https://fnaufel.github.io/publications/fnaufel-lc-00.pdf},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	booktitle = {European Summer Meeting of the Association for Symbolic Logic -- Logic Colloquium},
	title = {RETOOL: an Action Logic for Timed Transition Systems},
	year = {2000}
}

@inproceedings{fnaufelLsfa06,
	url = {https://fnaufel.github.io/publications/fnaufel-lsfa-06.pdf},
	address = {Natal, Rio Grande do Norte},
	abstract = {We define some topoi related to the topos of forests and illustrate how the internal language of such topoi can be used (via local set theory) to define logics where we can represent (meta)heuristic search strategies for solving computational problems.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	booktitle = {LSFA -- Brazilian Workshop on Logical and Semantic Frameworks, with Applications},
	title = {Topos-Based Logical Frameworks and an Application to (Meta)Heuristic Search},
	year = {2006}
}

@Report{fnaufelPuc02,
	url = {https://fnaufel.github.io/publications/fnaufel-puc-02.pdf},
	address = {Rio de Janeiro, Rio de Janeiro},
	abstract = {A specification language for real-time software systems is presented, along with a model-theoretic semantics. Notions from Category Theory are used to specify how the components of a system should interact. The potential role of the proposed language in the search for interoperability of specification formalisms is briefly discussed.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler and M. Endler},
	institution = {Depto. de Informática, PUC-Rio},
	number = {22/02},
	title = {A Real-Time Specification Language},
	year = {2002}
}

@Report{fnaufelPuc05,
	url = {https://fnaufel.github.io/publications/fnaufel-puc-05.pdf},
	address = {Rio de Janeiro, Rio de Janeiro},
	abstract = {We present a structural model for (meta)heuristic search strategies for solving computational problems. The model is defined through the use of topos-theoretical tools and techniques which provide an appropriate internal logic (with the language of Local Set Theory) where objects of interest can be represented.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	institution = {Depto. de Informática, PUC-Rio},
	number = {06/05},
	title = {A Logic-Based Formal Model for (Meta)Heuristics},
	year = {2005}
}

@Report{fnaufelPuc07,
	address = {Rio de Janeiro, Rio de Janeiro},
	url = {ftp://ftp.inf.puc-rio.br/pub/docs/techreports/07_25_rademaker.pdf},
	abstract = {Description Logics is a family of formalisms used to represent knowledge of a domain. In contrast with others knowledge representation systems, Description Logics are equipped with a formal, logic-based semantics. Knowledge representation systems based on description logics provide various inference capabilities that deduce implicit knowledge from the explicitly represented knowledge. We present a sequent calculus for ALC, a basic Description Logic. The first motivation  for developing such a system is the extraction of computational content of ALC proofs. The present calculus is an intermediate step towards a Natural Deduction System for ALC.},
	author = {A. Rademaker and Fernando Náufel do Amaral and E.H. Haeusler},
	ftp = {ftp://ftp.inf.puc-rio.br/pub/docs/techreports/07_25_rademaker.pdf <ftp://ftp.inf.puc-rio.br/pub/docs/techreports/07_25_rademaker.pdf>},
	institution = {Depto. de Informática, PUC-Rio},
	number = {25/07},
	title = {A Sequent Calculus for ALC},
	year = {2007}
}

@article{fnaufelRita00,
	journaltitle = {Revista de Informática Teórica e Aplicada},
	editor = {UFRGS},
	url = {https://fnaufel.github.io/publications/fnaufel-rita-00.pdf},
	abstract = {This paper discusses how RETOOL, an action logic featuring an operator that expresses necessary conditions, postconditions and time bounds of actions, can be combined with MTL, a linear-time temporal logic with time-bounded operators, to reason about general properties of timed transition systems, an abstract model for the behavior of objects in a real-time, object-oriented software system. The parallel composition of such objects, which can be modeled as a colimit in the category of RETOOL theories, is also discussed.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	number = {1},
	pages = {69--88},
	title = {A Logic-Based Approach for Real-Time Object-Oriented Software Development},
	volume = {VII},
	year = {2000}
}

@inproceedings{fnaufelSBGames2009,
	isbn = {978-972-789-299-0},
	url = {https://fnaufel.github.io/publications/fnaufel-sb-games-2009.pdf},
	address = {Rio de Janeiro, Rio de Janeiro},
	author = {A.F.V. Machado and Fernando Náufel do Amaral and E.W. Clua},
	booktitle = {Conferência de Ciências e Artes dos Videojogos 2009},
	title = {A Trivial Study Case of the Application of Ontologies in Electronic Games},
	year = {2009}
}

@inproceedings{fnaufelSemOnto2008,
	url = {https://fnaufel.github.io/publications/fnaufel-sem-onto-2008.pdf},
	address = {UFF, Niterói, Rio de Janeiro},
	abstract = {Abstract: Este trabalho apresenta esboços de modelos, uma abordagem baseada em semântica para visualização de descrições de conceitos em OWL.},
	author = {Fernando Náufel do Amaral},
	booktitle = {I Seminário de Pesquisa em Ontologia no Brasil},
	title = {Visualização de Descrições de Conceitos em OWL},
	year = {2008}
}

@inproceedings{fnaufelTIL2008,
	url = {https://fnaufel.github.io/publications/fnaufel-til-2008.pdf},
	address = {Vila Velha, Espírito Santo},
	abstract = {The development and use of ontologies may require users with no training in formal logic to handle complex concept descriptions (e.g., in the form of  necessary conditions in class definitions). To aid such users, alternative representations of concept descriptions have been proposed, such as natural language paraphrases and visualization frameworks. We examine examples of those representations and propose a novel visual framework, where more emphasis is placed on the semantics of concept descriptions than on their syntax.},
	author = {Fernando Náufel do Amaral},
	booktitle = {VI Workshop em Tecnologia da Informação e da Linguagem Humana (TIL)},
	title = {Visualizing the Semantics (Not the Syntax) of Concept Descriptions},
	year = {2008}
}

@Thesis{fnaufelThesis04,
	url = {http://www2.dbd.puc-rio.br/pergamum/biblioteca/php/mostrateses.php?open=1&arqtese=0016027_04_Indice.html},
	abstract = {This work employs concepts and tools from Category Theory and Topos Theory to construct a mathematical model for problems, reductions between problems, heuristic search spaces and strategies. More precisely, a search space construction strategy is represented by a functor from a certain category of problems to a certain category of forests. The collection of all such functors forms a topos, a specific model equipped with its own internal logic. This internal logic is then used to define search strategies and heuristics in Local Set Theory. Possible applications of this work include (1) the logical specification and classification of heuristics and metaheuristics used in practice and (2) a more abstract and general rendering of specific results relating the structure of problems to adequate problem-solving methods.},
	author = {Fernando Náufel do Amaral},
	note = {In Portuguese.},
	pdf = {http://www2.dbd.puc-rio.br/pergamum/biblioteca/php/mostrateses.php?open=1&arqtese=0016027_04_Indice.html <http://www2.dbd.puc-rio.br/pergamum/biblioteca/php/mostrateses.php?open=1&arqtese=0016027_04_Indice.html>},
	school = {Depto. de Informática, PUC-Rio},
	title = {Teoria de Modelos para Heurísticas Baseada em Topoi},
	year = {2004}
}

@Report{fnaufelUff97,
	address = {Niterói, Rio de Janeiro},
	author = {Fernando Náufel do Amaral and P.G. Rabelo},
	institution = {DCC, UFF},
	title = {Tradução de Estruturas de Controle para Sistemas de Tempo Real em Linguagens Orientadas a Objetos},
	year = {1997}
}

@inproceedings{fnaufelVorte06,
	url = {https://fnaufel.github.io/publications/fnaufel-vorte-06.pdf},
	address = {Hong Kong, China},
	abstract = {We present the structure of an ontology for Information Security (IS) and discuss a paradigm whereby it can be used to extract knowledge from natural language texts such as IS standards, security policies and security control descriptions. Besides providing a vocabulary for the IS domain, the proposed ontology stores logical forms corresponding to statements in the text, as well as a set of axioms used for inference in description logic (DL). We also describe a tool to provide automatic support for the formalization process.},
	author = {Fernando Náufel do Amaral and C. Bazílio and G.M.H. da Silva and A. Rademaker and E.H. Haeusler},
	booktitle = {Workshop on Vocabularies, Ontologies, and Rules for the Enterprise (VORTE)},
	title = {An Ontology-based Approach to the Formalization of Information Security Policies},
	year = {2006}
}

@inproceedings{fnaufelWmf00,
	url = {https://fnaufel.github.io/publications/fnaufel-wmf-00.pdf},
	address = {João Pessoa, Paraíba},
	abstract = {This paper discusses how RETOOL, an action logic featuring an operator that expresses necessary conditions, postconditions and time bounds of actions, can be combined with MTL, a linear-time temporal logic with time-bounded operators, to reason about general properties of timed transition systems, an abstract model for the behavior of objects in a real-time, object-oriented software system.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	booktitle = {Simpósio Brasileiro de Engenharia de Software -- Workshop de Métodos Formais},
	pages = {45--55},
	publisher = {SBC},
	title = {A Logic-Based Approach for Real-Time Object-Oriented Software Development},
	year = {2000}
}

@inproceedings{fnaufelWollic00,
	url = {https://fnaufel.github.io/publications/fnaufel-wollic-00.pdf},
	address = {Natal, Rio Grande do Norte},
	abstract = {This paper defines an action logic featuring an operator that denotes necessary conditions and postconditions of actions in a timed computational transition system. Three different semantics of the operator are discussed, and weak completeness is proved for one of them. It is also briefly shown how the action logic can be combined with a temporal logic to derive temporal properties of actions from the logical description of a real-time computational system.},
	author = {Fernando Náufel do Amaral and E.H. Haeusler},
	booktitle = {Workshop on Logic, Language, Information and Computation -- WoLLIC},
	pages = {123--132},
	title = {Completeness of an Action Logic Featuring a Delta-Operator for Timed Transition Systems},
	year = {2000}
}

@INPROCEEDINGS{fnaufelsemonto10,
	url = {https://fnaufel.github.io/publications/fnaufel-sem-onto-2010.pdf},
	address = {UFSC, Florianópolis, Santa Catarina},
	author = {Fernando Náufel do Amaral},
	title = {Usabilidade de uma Notação Diagramática para Descrições de Conceitos},
	booktitle = {III Seminário de Pesquisa em Ontologia no Brasil},
	abstract = {A informação presente em ontologias formais precisa frequentemente ser criada, consultada, ou alterada por usuários sem formação específica em Lógica e em linguagens formais. Neste contexto, técnicas e ferramentas para apresentar ontologias de forma intuitiva e de fácil compreensão são importantes. Neste artigo, discutimos os esboços de modelo, uma notação diagramática de nossa autoria para descrições de conceitos (um tipo específico de informação contido em uma ontologia). Para avaliar a facilidade de compreensão dos esboços de modelo, realizamos um teste de usabilidade comparando-os com Manchester OWL, uma notação textual também dirigida para usuários leigos. Relatamos aqui os resultados destes testes de usabilidade, que, além de indicar uma maior eficácia dos esboços de modelo, também apontam para aspectos específicos nos quais a nossa notação pode ser ainda melhorada.},
	year = {2010}
}

@article{fnaufelswj2013,
	editor = {IOS Press},
	url = {https://fnaufel.github.io/publications/fnaufel-swj-2013.pdf},
	abstract = {The development and use of ontologies may require users with no training in formal logic to handle complex concept descriptions. To aid such users, we propose a new visualization framework called “model outlines”, where more emphasis is placed on the semantics of concept descriptions than on their syntax. We present a rigorous definition of our visual language, as well as detailed algorithms for translating between model outlines and the Description Logic ALCN . We have recently conducted a usability study comparing model outlines and Manchester OWL; here, we report on its results, which indicate the potential benefits of our visual language for understanding concept descriptions},
	author = {Fernando Náufel do Amaral},
	journal = {Semantic Web},
	pages = {429--455},
	title = {Model Outlines: a Visual Language for DL Concept Descriptions},
	volume = {4},
	year = {2013}
}

@INPROCEEDINGS{fnaufelwwr2010,
	url = {https://fnaufel.github.io/publications/fnaufel-wrr-2010.pdf},
	address = {Bressanone/Brixen, Italy},
	publisher = {Springer},
	author = {Fernando Náufel do Amaral},
	title = {Usability of a Visual Language for DL Concept Descriptions},
	booktitle = {Proceedings of the Fourth International Conference on Web Reasoning and Rule Systems},
	series = {LNCS},
	volume = {6333},
	pages = {27--41},
	abstract = {The development and use of ontologies may require users with no training in formal logic to handle complex concept descriptions. To aid such users, we propose a new visualization framework called “model outlines”, where more emphasis is placed on the semantics of concept descriptions than on their syntax. We have conducted a usability study comparing model outlines and Manchester OWL, with results that indicate the potential benefits of our visual language for understanding concept descriptions.},
	year = {2010}
}