if ($_GET['lang']=="en")
echo "Papers in Proceedings";
else
echo "Artigos Completos em Anais de Eventos";
?>
if ($_GET['lang']=="en")
{ ?>
Uma Lógica para a Referência Ambígua by Andressa Sebben and Arthur Buchsbaum
XXXIII Conferência Latinoamericana de Informática, San José,Costa Rica, 2007
Abstract: This work presents a description logic named LAR – Logic of Ambiguous Reference – aiming to formalize suitably
situations of ambiguity and vacuity arising in natural languages and, implicitly, in mathematical discourse. A language
for it is described, together with a semantics and a sequent calculus. Some syntactic results and a theorem of
elimination of descriptions are also provided.
Um Método dos Tableaux
com um Refinamento para Evitar Repetições Desnecessárias de Fórmulas Universais
nos Ramos das Árvores de Prova, by Leticia Carvalho Pivetta Fendt and Arthur
Buchsbaum
Abstract: An enhancement of tableau method, non based on unification, aiming to diminish the number of nodes in proof trees and to increase probability of acquiring answers for a great number of questions. An algorithm, based on traditional tableau method for classical logic, uses an additional routine for controlling repetition of universal formulas in a given branch.
Um Método de Tableaux
por Prova Direta para a Lógica Proposicional Clássica, by Arthur Buchsbaum and Maurício Correia
Lemes Neto
XI Escola Regional de Informática, 2003, Londrina, Paraná, Brazil, pp. 14-22.
Abstract: A tableau method for classical propositional logic, in which the proof tree is developed from the original formula given as a possible conclusion of inference, instead of its negation, as it is done usually by refutation proofs.
A Logic for Ambiguous Description, by Arthur Buchsbaum
9th Workshop on Logic, Language, Information
and Computation, Rio de Janeiro, Brazil, 2002, pp. 149-166.
Abstract: A logic formalizing ambiguity, which appears both in natural language and in mathematical discourse, is presented, through a sequent calculus and a semantics, together with some elementary results.
Protótipo Inicial da Interface Gráfica de
um Provador de Teoremas, by Arthur Buchsbaum, Leticia Carvalho Pivetta
Fendt, Adriana F. Andrade and Natel Barreiros
I Seminário de Informática da UNIC, Proceedings of
I SEMINFO, 2002, Cuiabá, Mato Grosso, Brazil.
Um Método dos Tableaux
para evitar Repetições de Fórmulas nos Ramos das Árvores de Prova, by Arthur Buchsbaum and Leticia Carvalho
Pivetta Fendt
I Congresso de Informática de Rondônia, Proceedings of I CONINFO-RO, 2002, Ji-Paraná, Rondônia, Brazil, pp. 1-10
Abstract: An enhancement of tableau method, non based on unification, aiming to diminish the number of nodes in proof trees and to increase probability of acquiring answers for a great number of questions. An algorithm, based on traditional tableau method for classical logic, uses an additional routine for controlling repetition of universal formulas in a given branch.
A Positive Formalization
for the Notion of Pragmatic Truth, by Arthur Buchsbaum, Tarcisio Pequeno and Marcelino Pequeno
Abstract: A logic of pragmatic truth is presented, aiming to overcome some problems of a previous formalization by Newton C. A. da Costa and collaborators, which assigns a central role to logical possibility. It is argued that not being in conflict with assumed knowledge is not enough for considering true a proposition, that is only a necessary condition. A typical picture of the way a scientific theory evolves exhibit alternative hypotheses competing for expanding a theory. A pragmatic knowledge, in this stage of theory development, is one that can be considered true in face of all alternative hypotheses. The logic presented here formalizes this process of knowledge evolution.
O Método dos Tableaux
com Unificação, by Arthur Buchsbaum and Leticia Carvalho
Pivetta Fendt
III Encontro Nacional de Inteligência Artificial,
2001, Fortaleza, Ceará, Brazil.
Abstract: An enhancement of traditional tableau method, aiming to diminish the number of nodes of proof trees, and to increase probability of acquiring answers, based on unification procedure, commonly used in resolution method.
Automated Deduction with Non Classical Negations, by Arthur Buchsbaum and Tarcisio Pequeno
3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1994, pp. 51-64.
Abstract: Three basic alternatives to classical negation, represented by paraconsistent calculus C1, the paracomplete calculus P1, and the non alethic calculus N1, all defined by Newton C. A. da Costa. For each of these calculi it is provided a corresponding tableau system. A general proof of correctness and completeness is given, including as special cases these three systems.
Sensible Inconsistent Reasoning: A Tableau
System for LEI, by Marcelo Correa, Arthur Buchsbaum and Tarcisio Pequeno
Technical Notes of AAAI Fall Symposium on Automated Deduction in Non-Standard Logics, 1993.
Abstract: A proof method based on tableaux for a subset of the Logic of Epistemic Inconsistency, suitable as a basis for automatizing a logic of defaults.
Raciocínio Automático com Conhecimento Incompleto
e Inconsistente I: um Sistema de Tableaux para LEI, by Marcelo Correa, Arthur Buchsbaum and Tarcisio
Pequeno
Proceedings of IX Simpósio Brasileiro de Inteligência Artificial, 1992, pp. 281-296.
Abstract: A proof method based on tableaux for a subset of the Logic of Epistemic Inconsistency, suitable as a basis for automatizing a logic of defaults.
The Logic of Epistemic Inconsistency, by Arthur Buchsbaum and Tarcisio Pequeno
Proceedings of the Second International Conference on Principles of Knowledge Representation and Reasoning, 1991, pp. 453-460.
Republished in Proceedings of 10th Brazilian Conference on Mathematical Logic, 1995, pp. 177-197.
Abstract: It is introduced the idea of epistemic inconsistency, referring to contradictory viewpoints about a same situation. Such contradictions don't reflect an anomalous behavior of state of affairs, but incompleteness or vagueness of our knowledge about it. Association of this phenomenon with non monotonic reasoning is discussed. A logic, its calculus and semantics, aiming to precise this notion and to represent reasoning about contradictory views, without implying triviality, is presented.
Um Provador Paraconsistente, by Arthur Buchsbaum and Tarcisio Pequeno
5o Simpósio Brasileiro de Inteligência Artificial, Brazil, 1988, pp. 531-540.
Published also by IV Reunião de Trabalho do Projeto ESTRA, Coletânea de Resultados de Pesquisas, SID Informática, Brazil, 1988, pp. 173-182.
Abstract: An automated proof method for a paraconsistent logic, the calculus C1* of Newton C. A. da Costa. Actually two tableau systems were constructed: one with a small number of rules, from which the correctness and completeness of the method was proved, and other one, equivalent to the former, is a system of derived rules, which was implemented.
Uma Lógica para a Referência Ambígua de Andressa Sebben e Arthur Buchsbaum
XXXIII Conferência Latinoamericana de Informática, San José, Costa Rica, 2007.
Resumo: Este trabalho apresenta uma lógica descritiva denominada LAR – Lógica da Referência Ambígua – visando formalizar
adequadamente situações de ambiguidade e vacuidade presentes nas linguagens naturais e, implicitamente, no discurso
matemático. Uma linguagem para a mesma é descrita, juntamente com uma semântica e um cálculo de sequentes.
Alguns resultados sintáticos e um teorema de eliminação das descrições são também apresentados.
Um Método dos Tableaux
com um Refinamento para Evitar Repetições Desnecessárias de Fórmulas Universais
nos Ramos das Árvores de Prova, de Leticia Carvalho Pivetta Fendt e Arthur
Buchsbaum
Resumo: Um refinamento ao método dos tableaux, não baseado em unificação,
visando diminuir o número de nós das árvores de prova e aumentar a probabilidade
de obtenção de respostas para um número maior de problemas. Um algoritmo,
baseado no método tradicional dos tableaux para a lógica clássica, recorre
a uma rotina adicional para controlar a repetição de fórmulas universais
em um dado ramo.
Um Método de Tableaux
por Prova Direta para a Lógica Proposicional Clássica, de Arthur Buchsbaum e Maurício Correia
Lemes Neto
XI Escola Regional de Informática, 2003, Londrina,
Paraná, pgs. 14-22.
Resumo: Um método de tableaux para a Lógica Proposicional Clássica, no qual
a árvore de prova é desenvolvida a partir da própria fórmula dada como possível
conclusão da inferência, ao invés de sua negação, como é feito tradicionalmente
em provas por refutação.
A Logic for Ambiguous
Description, de Arthur Buchsbaum
9th Workshop on Logic, Language, Information
and Computation, Rio de Janeiro, 2002, pgs. 149-166.
Resumo: Uma lógica que formaliza a ambigüidade, a qual está presente tanto
na linguagem natural como no discurso matemático, é apresentada, através
de um cálculo de seqüentes e de uma semântica, juntamente com alguns resultados
elementares.
Protótipo Inicial da Interface Gráfica de
um Provador de Teoremas, de Arthur Buchsbaum, Leticia Carvalho Pivetta
Fendt, Adriana F. Andrade e Natel Barreiros
I Seminário de Informática da UNIC, Anais do
I SEMINFO, 2002, Cuiabá, Mato Grosso.
Um Método dos Tableaux
para evitar Repetições de Fórmulas nos Ramos das Árvores de Prova, de Arthur Buchsbaum e Leticia Carvalho
Pivetta Fendt
I Congresso de Informática de Rondônia, Anais
do I CONINFO-RO, 2002, Ji-Paraná, Rondônia, pgs. 1-10
Resumo: Um refinamento ao método dos tableaux, não baseado em unificação,
visando diminuir o número de nós das árvores de prova e aumentar a probabilidade
de obtenção de respostas para um número maior de problemas. Um algoritmo,
baseado no método tradicional dos tableaux para a lógica clássica, recorre
a uma rotina adicional para controlar a repetição de fórmulas universais
em um dado ramo.
A Positive Formalization
for the Notion of Pragmatic Truth, de Arthur Buchsbaum, Tarcisio Pequeno e
Marcelino Pequeno
Resumo: Uma lógica da verdade pragmática buscando superar problemas de uma
formalização prévia apresentada por Newton C. A. da Costa e colaboradores,
a qual atribui um papel central à possibilidade lógica. É argüido que não
estar em conflito com o conhecimento assumido não é suficiente para considerar
uma proposição como verdadeira; isto é apenas uma condição necessária. Um
quadro típico do modo pelo qual uma teoria científica evolui exibe hipóteses
alternativas competindo para expandir a teoria. Um conhecimento pragmático,
neste estágio de desenvolvimento da teoria, é aquele que pode ser considerado
verdadeiro diante de todas as hipóteses alternativas. A lógica aqui apresentada
formaliza este processo de evolução do conhecimento.
O Método dos Tableaux
com Unificação, de Arthur Buchsbaum e Leticia Carvalho
Pivetta Fendt
III Encontro Nacional de Inteligência Artificial,
2001, Fortaleza, Ceará.
Resumo: Um refinamento sobre o método dos tableaux, tal como tradicionalmente
apresentado, visando diminuir o número de nós das árvores de prova, bem
como aumentar a possibilidade de obtenção de respostas, baseado no procedimento
de unificação, comumente utilizado no método da resolução.
Automated Deduction with Non Classical Negations,
de Arthur Buchsbaum e Tarcisio Pequeno
3rd Workshop on Theorem Proving with Analytic
Tableaux and Related Methods, 1994, pgs. 51-64.
Resumo: Três alternativas básicas à
negação clássica, representadas pelo cálculo
paraconsistente C1, o cálculo paracompleto
P1, e o cálculo não alético
N1, todos definidos por Newton C. A. da Costa.
Para cada um destes cálculos é dado um sistema de tableaux
correspondente. É exposta uma prova geral de correção
e completude, incluindo como casos particulares estes três sistemas.
Sensible Inconsistent Reasoning: A Tableau
System for LEI, de Marcelo Correa, Arthur Buchsbaum e Tarcisio
Pequeno
Technical Notes of AAAI Fall Symposium on Automated
Deduction in Non-Standard Logics, 1993.
Resumo: Um método de prova baseado em tableaux
para um subconjunto da Lógica da Inconsistência Epistêmica,
adequado como base para uma automatização de uma lógica
de defaults.
Raciocínio Automático com Conhecimento Incompleto
e Inconsistente I: um Sistema de Tableaux para LEI, de Marcelo Correa, Arthur Buchsbaum e Tarcisio
Pequeno
Anais do IX Simpósio Brasileiro de Inteligência
Artificial, 1992, pgs. 281-296.
Resumo: Um método automático de prova baseado
em tableaux para um subconjunto da Lógica da Inconsistência
Epistêmica, adequado como base para uma automatização
de uma lógica de defaults.
The Logic of Epistemic Inconsistency, de Arthur Buchsbaum e Tarcisio Pequeno
Proceedings of the Second International Conference
on Principles of Knowledge Representation and Reasoning,
1991, pgs. 453-460.
Republicado por Proceedings of 10th Brazilian Conference on Mathematical Logic,
1995, pgs. 177-197.
Resumo: A noção de inconsistência
epistêmica, referindo-se a visões contraditórias sobre
uma mesma situação, é introduzida. Tais contradições
não refletem um comportamento anômalo do estado das coisas,
mas sim a incompletude ou vagueza de nosso conhecimento acerca deste. A
associação deste fenômeno com o raciocínio não
monotônico é debatida. Uma lógica, o seu cálculo
e semântica, visando tornar precisa esta noção e viabilizar
o raciocínio envolvendo visões contraditórias, sem
acarretar trivialidade, é apresentada.
Um Provador Paraconsistente, de Arthur Buchsbaum e Tarcisio Pequeno
Anais do V Simpósio Brasileiro de Inteligência
Artificial, 1988, pgs. 531-540.
Publicado também por IV Reunião de Trabalho do Projeto ESTRA, Coletânea de
Resultados de Pesquisas, SID Informática, 1988, pgs 173-182.
Resumo: Um método de prova automático para uma lógica
paraconsistente, o cálculo C1* de Newton C.
A. da Costa, é apresentado. Trata-se de um método analítico utilizando um
sistema de tableaux. Na realidade, dois sistemas de tableaux foram elaborados:
um com um número pequeno de regras, a partir do qual são provadas a consistência
e a completude do método, e outro, que mostramos ser equivalente ao primeiro,
é um sistema de regras derivadas a partir do qual foi realizada uma implementação.
Este artigo apresenta a minha dissertação de mestrado de uma forma concisa.