Another paper from members of the ConsRel project:
Towards an Efficient Prover for the C1 Paraconsistent Logic
Authors: Adolfo Netoa, 1, 
, Celso A.A. Kaestnera, and Marcelo Fingerb,
Abstract
The KE inference system is a tableau method developed by Marco Mondadori which was presented as an improvement, in the computational efficiency sense, over Analytic Tableaux. In the literature, there is no description of a theorem prover based on the KE method for the C1 paraconsistent logic. Paraconsistent logics have several applications, such as in robot control and medicine. These applications could benefit from the existence of such a prover. We present a sound and complete KE system for C1, an informal specification of a strategy for the C1 prover as well as problem families that can be used to evaluate provers for C1. The C1 KE system and the strategy described in this paper will be used to implement a KE based prover for C1, which will be useful for those who study and apply paraconsistent logics.
Keywords: tableaux systems; KE system; C1 logic; paraconsistent logics; problem families
Another publication from members of the ConsRel projetct:
Paraconsistent Machines and their Relation to Quantum Computing
http://logcom.oxfordjournals.org/cgi/content/abstract/exp072v1?ijkey=Ver5JBNUijUJdp6&keytype=ref
Juan C. Agudelo, Ph.D.
Walter Carnielli
Abstract
We describe a method to axiomatize computations in deterministic Turing machines (TMs). When applied to computations in non-deterministic TMs, this method may produce contradictory (and therefore trivial) theories, considering classical logic as the underlying logic. By substituting in such theories the underlying logic by a paraconsistent logic we define a new computation model, the paraconsistent Turing machine. This model allows a partial simulation of superposed states of quantum computing. Such a feature allows the definition of paraconsistent algorithms which solve (with some restrictions) the well-known Deutsch’s and Deutsch-Jozsa problems. This first model of computation, however, does not adequately represent the notions of entangled states and relative phase, which are key features in quantum computing. In this way, a more sharpened model of paraconsistent TMs is defined, which better approaches quantum computing features. Finally, we define complexity classes for such models, and establish some relationships with classical complexity classes.
Keywords: Paraconsistent Turing machines; paraconsistent computation; quantum computation; Deutsch’s problem; Deutsch-Jozsa problem; entangled states
A new paper from members of the ConsRel project:
“Interpolation via translations”
João Rasga,Walter Carnielli e Cristina Sernadas
Math. Log. Quart. 55, No. 5, 515-534 (2009) / DOI 10.1002/malq.200810013
http://www3.interscience.wiley.com/journal/117943446/grouphome/home.html
Abstract:
“A new technique is presented for proving that a consequence system enjoys Craig interpolation or Maehara interpolation based on the fact that these properties hold in another consequence system. This technique is based on the existence of a back and forth translation satisfying some properties between the consequence systems. Some examples of translations satisfying those properties are described. Namely a translation between the global/local consequence systems induced by fragments of linear
logic, a Kolmogorov-Gentzen-Gödel style translation, and a new translation between the global consequence systems induced by full Lambek calculus and linear logic, mixing features of a Kiriyama-Ono style translation with features of a Kolmogorov-Gentzen- Gödel style translation. These translations establish a strong relationship between the logics involved and are used to obtain new results about whether Craig interpolation and Maehara interpolation hold in that logics.”
A new paper from ConsRel members has been published:
Base Revision for Ontology Debugging
Márcio M. Ribeiro and Renata Wassermann
Department of Computer Science, Institute of Mathematics and Statistics, University of São Paulo, Brazil.
E-mail: marciomr AT ime.usp.br,renata AT ime.usp.br
Abstract: Belief Revision deals with the problem of adding new information to a knowledge base in a consistent way. Ontology Debugging, on the other hand, aims to find the axioms in a terminological knowledge base which caused the base to become inconsistent. In this article, we propose a belief revision approach in order to find and repair inconsistencies in ontologies represented in some description logic (DL). As the usual belief revision operators cannot be directly applied to DLs, we propose new operators that can be used with more general logics and show that, in particular, they can be applied to the logics underlying OWL-DL and Lite.
Keywords: Belief Revision; Ontology Evolution; Description Logics
Published in the Journal of Logic and Computation.
Link http://logcom.oxfordjournals.org/cgi/content/abstract/19/5/721
Bibtex entry:
@article{RibeiroWasserman09,
author = {Ribeiro, Marcio M. and Wassermann, Renata},
doi = {10.1093/logcom/exn048},
journal = {J Logic Computation},
month = {October},
number = {5},
pages = {721–743},
posted-at = {2009-09-22 15:52:38},
priority = {2},
title = {Base Revision for Ontology Debugging},
url = {http://dx.doi.org/10.1093/logcom/exn048},
volume = {19},
year = {2009}
}
Another article written by members of the ConsRel project was accepted for publication:
Agudelo, Juan C. and Carnielli, Walter. Paraconsistent Machines and their Relation to Quantum Computing. Accepted for publication in the Journal of Algorithms in Cognition, Informatics and Logic. A preprint of this article is available at http://arxiv.org/abs/0802.0150.
This article is related to a previously published article written by the same authors:
A new paper from ConsRel members has been published:
On Graph-theoretic Fibring of Logics
Amilcar Sernadas, Cristina Sernadas and Joao Rasga
Department of Mathematics, Instituto Superior Técnico, TU Lisbon and SQIG, Instituto de Telecomunicações, Lisbon, Portugal.
Marcelo Coniglio
Department of Philosophy and CLE, State University of Campinas, Brazil.
E-mail: coniglio@cle.unicamp.br
Received 29 July 2008.
Abstract
A graph-theoretic account of fibring of logics is developed, capitalizing on the interleaving characteristics of fibring at the linguistic, semantic and proof levels. Fibring of two signatures is seen as a multi-graph (m-graph) where the nodes and the m-edges include the sorts and the constructors of the signatures at hand. Fibring of two models is a multi-graph (m-graph) where the nodes and the m-edges are the values and the operations in the models, respectively. Fibring of two deductive systems is an m-graph whose nodes are language expressions and the m-edges represent the inference rules of the two original systems. The sobriety of the approach is confirmed by proving that all the fibring notions are universal constructions. This graph-theoretic view is general enough to accommodate very different fibrings of propositional based logics encompassing logics with non-deterministic semantics, logics with an algebraic semantics, logics with partial semantics and substructural logics, among others. Soundness and weak completeness are proved to be preserved under very general conditions. Strong completeness is also shown to be preserved under tighter conditions. In this setting, the collapsing problem appearing in several combinations of logic systems can be avoided.
Keywords: Fibring; graph-theoretic techniques; preservation results; combination of logics; collapsing problem
Link: http://logcom.oxfordjournals.org/cgi/content/abstract/exp024v1?etoc
The bibtex entry for this publication is:
@article{Consrel_2009_Coniglio_b,
abstract = {A graph-theoretic account of fibring of logics is developed, capitalizing on the interleaving characteristics of fibring at the linguistic, semantic and proof levels. Fibring of two signatures is seen as a multi-graph (m-graph) where the nodes and the m-edges include the sorts and the constructors of the signatures at hand. Fibring of two models is a multi-graph (m-graph) where the nodes and the m-edges are the values and the operations in the models, respectively. Fibring of two deductive systems is an m-graph whose nodes are language expressions and the m-edges represent the inference rules of the two original systems. The sobriety of the approach is confirmed by proving that all the fibring notions are universal constructions. This graph-theoretic view is general enough to accommodate very different fibrings of propositional based logics encompassing logics with non-deterministic semantics, logics with an algebraic semantics, logics with partial semantics and substructural logics, among others. Soundness and weak completeness are proved to be preserved under very general conditions. Strong completeness is also shown to be preserved under tighter conditions. In this setting, the collapsing problem appearing in several combinations of logic systems can be avoided. 10.1093/logcom/exp024},
author = {Sernadas, Amilcar and Sernadas, Cristina and Rasga, Joao and Coniglio, Marcelo},
citeulike-article-id = {5086624},
citeulike-linkout-0 = {http://dx.doi.org/10.1093/logcom/exp024},
doi = {10.1093/logcom/exp024},
journal = {J Logic Computation},
month = {July},
pages = {exp024+},
posted-at = {2009-07-07 14:47:57},
priority = {2},
title = {On Graph-theoretic Fibring of Logics},
url = {http://dx.doi.org/10.1093/logcom/exp024},
year = {2009}
}
A new paper from ConsRel members has been published:
A Graph-theoretic Account of Logics
Amilcar Sernadas, Cristina Sernadas and Joao Rasga – Department of Mathematics, Instituto Superior Técnico, TU Lisbon and SQIG, Instituto de Telecomunicações, Lisbon, Portugal.
Marcelo Coniglio – Department of Philosophy and CLE, State University of Campinas, Brazil.
Abstract: A graph-theoretic account of logics is explored based on the general notion of m-graph (i.e; a graph where each edge can have a finite sequence of nodes as source). Signatures, interpretation structures and deduction systems are seen as multi-graphs (m-graphs). After defining a category freely generated by a m-graph, formulas and expressions in general can be seen as morphisms. Moreover, derivations involving rule instantiation are also morphisms. Soundness and completeness theorems are proved. As a consequence of the generality of the approach our results apply to very different logics encompassing, among others, substructural logics as well as logics with non-deterministic semantics, and subsume all logics endowed with an algebraic semantics.
Keywords: Graph-theoretic account of logics; non-deterministic semantics; diagrammatic reasoning via morphisms; completeness results
Link: http://logcom.oxfordjournals.org/cgi/content/refs/exp023v1
The bibtex entry for this publication is:
@article{Consrel_2009_coniglio,
abstract = {A graph-theoretic account of logics is explored based on the general notion of m-graph (i.e; a graph where each edge can have a finite sequence of nodes as source). Signatures, interpretation structures and deduction systems are seen as multi-graphs (m-graphs). After defining a category freely generated by a m-graph, formulas and expressions in general can be seen as morphisms. Moreover, derivations involving rule instantiation are also morphisms. Soundness and completeness theorems are proved. As a consequence of the generality of the approach our results apply to very different logics encompassing, among others, substructural logics as well as logics with non-deterministic semantics, and subsume all logics endowed with an algebraic semantics. 10.1093/logcom/exp023},
author = {Sernadas, Amilcar and Sernadas, Cristina and Rasga, Joao and Coniglio, Marcelo },
doi = {10.1093/logcom/exp023},
journal = {J Logic Computation},
month = {April},
pages = {exp023+},
posted-at = {2009-04-23 18:58:56},
priority = {2},
title = {A Graph-theoretic Account of Logics},
url = {http://dx.doi.org/10.1093/logcom/exp023},
year = {2009}
}
Reports submitted to and approved by FAPESP
- Report 4 (2009) – PDF: http://www.cle.unicamp.br/principal/grupoglta/Thematic-Consrel-FAPESP/Report-04-2009/Report04.pdf
- Report 3 (2008) – PDF: http://www.cle.unicamp.br/principal/grupoglta/Thematic-Consrel-FAPESP/Report-03-2008/Report03.pdf
- Report 2 (2007) – PDF: http://www.cle.unicamp.br/principal/grupoglta/Thematic-Consrel-FAPESP/Report-02-2007/Report02.pdf
- Report 1 (2006) – PDF: http://www.cle.unicamp.br/principal/grupoglta/Thematic-Consrel-FAPESP/Report-01-2006/Report01.pdf
- All reports and published work: http://www.cle.unicamp.br/principal/grupoglta/Thematic-Consrel-FAPESP/
Source: http://consrel.incubadora.fapesp.br/portal/publications/reports
KEMS is a KE-based Multi-Strategy theorem prover. The KE system, a tableau method developed by Marco Mondadori and Marcello D’Agostin, was presented as an improvement, in the computational efficiency sense, over the Analytic Tableau method. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. A multi-strategy theorem prover can be used for three purposes: educational, exploratory and adaptive. For educational purposes, it can be used to illustrate how the choice of a strategy can affect performance of the prover. As an exploratory tool, a multi-strategy theorem prover can be used to test new strategies and compare them with others. And we can also think of an adaptive multi-strategy theorem prover that changes the strategy used according to features of the problem presented to it.
KEMS was developed as Adolfo Gustavo Serra Seca Neto’s PhD. project, advised by Marcelo Finger. KEMS is implemented in Java and AspectJ. Java is a well established object-oriented programming language and AspectJ is the major representative of a new programming paradigm: aspect-oriented programming.
KEMS’s newest version is avaliable at: http://www.dainf.ct.utfpr.edu.br/~adolfo/KEMS
