Alessandra Russo

We investigate the semantics of the logical systems obtained by introducing the modalities and into the family of substructural implication logics (including relevant, linear and intuitionistic implication). Then, in the spirit of the LDS (Labelled Deductive Systems) methodology, we "import" this semantics into the classical proof system KE. This leads to the formulation of a uniform labelled refutation system for the new logics which is a natural extension of a system for substructural implication developed by the first two authors in a previous paper.

In this article, we propose a belief revision approach for families of (non-classical) logics whose semantics are first-order axiomatisable. Given any such (non-classical) logic , the approach enables the definition of belief revision operators for , in terms of a belief revision operation satisfying the postulates for revision theory proposed by Alchourrrdenfors and Makinson (AGM revision, Alchourrukasiewicz's many-valued logic. In addition, we present a general methodology to translate algebraic logics into classical logic. For the examples provided, we analyse in what circumstances the properties of the AGM revision are preserved and discuss the advantages of the approach from both theoretical and practical viewpoints

In this paper a uniform methodology to perform natural\ndeduction over the family of linear, relevance and intuitionistic\nlogics is proposed. The methodology follows the Labelled\nDeductive Systems (LDS) discipline, where the deductive process\nmanipulates {\em declarative units} -- formulas {\em labelled}\naccording to a {\em labelling algebra}. In the system described\nhere, labels are either ground terms or variables of a given {\em\nlabelling language} and inference rules manipulate formulas and\nlabels simultaneously, generating (whenever necessary)\nconstraints on the labels used in the rules. A set of natural\ndeduction style inference rules is given, and the notion of a\n{\em derivation} is defined which associates a labelled natural\ndeduction style ``structural derivation'' with a set of generated\nconstraints. Algorithmic procedures, based on a technique called\n{\em resource abduction\/}, are defined to solve the constraints\ngenerated within a structural derivation, and their termination\nconditions discussed. A natural deduction derivation is then\ndefined to be {\em correct} with respect to a given substructural\nlogic, if, under the condition that the algorithmic procedures\nterminate, the associated set of constraints is satisfied with\nrespect to the underlying labelling algebra. Finally, soundness\nand completeness of the natural deduction system are proved with\nrespect to the LKE tableaux system \cite{daga:LAD}.\footnote{Full\nversion of a paper presented at the {\em 3rd Workshop on Logic,\nLanguage, Information and Computation\/} ({\em WoLLIC'96\/}), May\n8--10, Salvador (Bahia), Brazil, organised by Univ.\ Federal de\nPernambuco (UFPE) and Univ.\ Federal da Bahia (UFBA), and\nsponsored by IGPL, FoLLI, and ASL.}

K. Broda, Dov M. Gabbay, Alessandra Russo and LuÍs C. Lamb argue that though the many families of logic may seem to differ in their logical nature, it is possible to provide them with a unifying logical framework whenever their semantics is axiomatizable in first-order logic. They provide such a framework based on the labeled deductive system methodology, and demonstrate how it works in such families as normal modal logics, conditional logics of normality, the modal logic of elsewhere, the multiplicative fragment of substructural linear logic, and Lukasiewicz fuzzy logic.

This paper introduces a proof procedure that integrates Abductive Logic Programming and Inductive Logic Programming to automate the learning of first order Horn clause theories from examples and background knowledge. The work builds upon a recent approach called Hybrid Abductive Inductive Learning by showing how language bias can be practically and usefully incorporated into the learning process. A proof procedure for HAIL is proposed that utilises a set of user-specified mode declarations to learn hypotheses that satisfy a given language bias. A semantics is presented that accurately characterises the intended hypothesis space and includes the hypotheses derivable by the proof procedure. An implementation is described that combines an extension of the Kakas-Mancarella ALP procedure within an ILP procedure that generalises the Progol system of Muggleton. The explicit integration of abduction and induction is shown to allow the derivation of multiple clause hypotheses in response to a single seed example and to enable the inference of missing type information in a way not previously possible