The Interest Group in Pure and Applied Logics (IGPL) and the European Association for Logic, Language and Information (FoLLI) are happy to announce the annual prize for the best idea of the year in the area of pure and applied logic.
There are many prizes in the community and they are usually won by leading researchers with an established body of research. However, progress also depends on fresh insights and sudden ideas, often coming from young people in the field. It is the latter ideas that we want to encourage.
We therefore invite nominations for the second US$ 1000 annual
We are thinking of solutions to challenging open questions, but also of attractive new research ideas, novel connections between different aspects of logic, language and computation, etcetera. These should be surprising, and enhance the connectivity in our field.
We call upon IGPL and FoLLI members and any other researchers in pure and applied logic to put forward candidates, who came out with a prize worthy good idea in 1995. It should be an idea published or in preprint during the year. In certain cases, we are also prepared to consider prize essays written precisely for this purpose. Proposals with personal background and case for support should be sent to the FoLLI chairman,
Professor Wilfrid Hodges
The prize committee consists of the FoLLI chairman, the editorial board of the Journal of the IGPL and the FoLLI board members. Deadline for proposals for the 1995 prize is 1 May 1996.
The top five candidates will be invited to publish their ideas in a special issue of the Journal of the IGPL and the committee will write an editorial describing the importance of these ideas.
Back to the table of contents.
In categorical proof theory, propositions and proofs are presented as objects and arrows in a category. It thus embodies the strong constructivist paradigms of propositions-as-types and proofs-as-constructions, which lie in the foundation of computational logic. Moreover, in the categorical setting, a third paradigm arises, not available elsewhere: logical-operations-as-adjunctions. It offers an answer to the notorious question of the equality of proofs. So we chase diagrams in algebra of proofs.
On the basis of these ideas, the present paper investigates proof theory of regular logic: the &amm;exists-fragment of the first order logic with equality. The corresponding categorical structure is regular fibration. The examples include stable factorisations, sites, triposes. Regular logic is exactly what is needed to talk about maps, as total and single-valued relations. However, when enriched with proofs-as-arrows, this familiar concept must be supplied with an additional conversion rule, connecting the proof of the totality with the proof of the single-valuedness. We explain the logical meaning of this rule, and then determine precise conditions under which a regular fibration supports the principle of function comprehension (that each map corresponds to a unique function viz arrow in the base), thus lifting a basic theorem from regular categories (e.g. [2.132]{FreydScedrov}), recently relativized to factorisation systems [Kelly,mapsI]. The obtained results bring us a step closer to extending the WP-set construction [HJP] from triposes to non-posetal fibrations, and thus closer to `toposes' accommodating categorical proof theory.
Get the
.dvi (75 KB) or the
PostScript (243 KB) file.
Back to the table of contents.
Twan Laan
Department of Mathematics and Computing Science,
Eindhoven University of Technology,
P.O. Box 513, 5600 MB Eindhoven, The Netherlands.
E-mail: laan@win.tue.nl
Both in Kripke's Theory of Truth KTT [krip75] and Russell's Ramified Type Theory RTT [whit10,laan94] we are confronted with some hierarchy. In RTT, we have a double hierarchy of orders and types. That is, the class of propositions is divided into different orders where a propositional function can only depend on objects of lower orders and types. Kripke on the other hand, has a ladder of languages where the truth of a proposition in language L_n can only be made in L_m where m > n. Kripke finds a fixed point for his hierarchy (something Russell does not attempt to do). We investigate in this paper the similarities of both hierarchies: At level n of KTT the truth or falsehood of all order-n-propositions of RTT can be established. Moreover, there are order-n-propositions that get a truth value at an earlier stage in KTT. Furthermore, we show that RTT is more restrictive than KTT, as some type restrictions are not needed in KTT and more formulas can be expressed in the latter.
Looking back at the double hierarchy of Russell, Ramsey [rams25], and Hilbert and Ackermann [hilbacke28] considered the orders to cause the restrictiveness, and therefore removed them. This removal resulted in Church's Simple Type Theory [STT] [chur40]. We show however that orders in RTT correspond to levels of truth in KTT. Hence, KTT can be regarded as the dual of [STT] where types have been removed and orders are maintained. As RTT is more restrictive than KTT, we can conclude that it is the combination of types and orders that was the restrictive factor in RTT.
Get the
.dvi (39 KB) or the
PostScript (213KB) file.
Back to the table of contents.
Norman D. Megill
19 Locke Lane, Lexington, MA 02173, USA
E-mail: ndm@shore.net
Martin W. Bunder
Department of Mathematics, University of Wollongong,
Wollongong NSW 2500, Australia.
E-mail: Martin_Bunder@uow.edu.au
BB'IW logic (or T->) is known to be D-complete. This paper shows that there are infinitely many weaker D-complete logics and it also examines how certain D-incomplete logics can be made complete by altering their axioms using simple substitutions.
Get the
.dvi (14 KB) or the
PostScript (181 KB) file.
Back to the table of contents.
L. De Raedt
Department of Computer Science, Katholieke Universiteit Leuven,
Celestijnenlaan 200A, B-3001 Heverlee, Belgium.
E-mail: Luc.DeRaedt@cs.kuleuven.ac.be
Nada Lavrac
Department of Intelligent Systems,
Jozef Stefan Institute, Jamova 39, 1001 Ljubljana, Slovenia.
E-mail: Nada.Lavrac@ijs.si
Inductive logic programming (ILP) is a research area which has its roots in inductive machine learning and computational logic. The paper gives an introduction to this area based on a distinction between two different semantics used in inductive logic programming, and illustrates their application in knowledge discovery and programming. Whereas most research in inductive logic programming has focussed on learning single predicates from given datasets using the normal ILP semantics (e.g. the well known ILP systems GOLEM and FOIL), the paper investigates also the non-monotonic ILP semantics and the learning problems involving multiple predicates. The non-monotonic ILP setting avoids the order dependency problem of the normal setting when learning multiple predicates, extends the representation of the induced hypotheses to full clausal logic, and can be applied to different types of application.
Get the
.dvi (46 KB) or the
PostScript (214 KB) file.
Back to the table of contents.
Michael Fisher
Department of Computing,
Manchester Metropolitan University,
Chester Street,
Manchester M1 5GD, United Kingdom
E-mail: M.Fisher@doc.mmu.ac.uk
Anthony Hunter, Richard Owens
Department of Computing,
Imperial College of Science, Technology and Medicine,
180 Queen's Gate,
London SW7 2BZ, UK.
E-mail: {abh,
rpo}@doc.ic.ac.uk
Howard Barringer
Department of Computer Science,
University of Manchester,
Oxford Road,
Manchester M13 9PL, UK.
E-mail: howard@cs.man.ac.uk
Dov Gabbay
Department of Computing,
Imperial College of Science, Technology and Medicine,
180 Queen's Gate,
London SW7 2BZ, UK.
E-mail: dg@doc.ic.ac.uk
Graham Gough
Department of Computer Science,
University of Manchester,
Oxford Road,
Manchester M13 9PL, UK.
E-mail: grahamcs.man.ac.uk
Ian Hodkinson
Department of Computing,
Imperial College of Science, Technology and Medicine,
180 Queen's Gate,
London SW7 2BZ, UK.
E-mail: imh@doc.ic.ac.uk
Peter Mc Brien
King's College,
Dept of Computer Science,
The Strand,
London WC2R 2LS,
E-mail: {pjm@dcs.kcl.ac.uk
Mark Reynolds
King's College,
Dept of Computer Science,
The Strand,
London WC2R 2LS,
E-mail: markr@dcs.kcl.ac.uk
Derek Brough
Department of Computing,
Imperial College of Science, Technology and Medicine,
180 Queen's Gate,
London SW7 2BZ, UK.
E-mail: drb@doc.ic.ac.uk
Meta-languages are vital to the development and usage of formal systems, and yet the nature of meta-languages and associated notions require clarification. Here we attempt to provide a clear definition of the requirements for a language to be a meta-language, together with consideration of issues of proof theory, model theory and interpreters for such a language.
Get the
.dvi (29 KB) or the
PostScript (194 KB) file.
Back to the table of contents.
In this paper the ultrafilter properties of canonical frames are used to produce a non-standard map between canonical frames of different cardinalities. While this map is not a p-morphism, it is presented as a step towards the full understanding of canonical structures.
Get the
.dvi (19 KB) or the
PostScript (185 KB) file.
Back to the table of contents.
The paper studies the admissibility of some cancellation rules in normal
modal systems with the Brouwerian axiom. For example, KDB and KTB are
proved to admit the following rule:
if |- -(a & b) and
|- <>a = <>b
then |- <> -(a v b).
Two notions of the preservation of
validity by a rule on a frame are defined; on both, the preservation of
validity by the preceding rule is shown
not to be a first-order condition. A speculative connection is suggested
with logics of vagueness.
Get the
.dvi (40 KB) or the
PostScript (212 KB) file.
Back to the table of contents.
This book examines the concepts of knowledge and belief and their formalization in systems of epistemic logic, concepts which are equally central to philosophy and artificial intelligence research (AI). The original contributions compiled in Knowledge and Belief in Philosophy and Artificial Intelligence give an excellent overview of the current state of research in a field which has now developed into one of the focal areas of knowledge representation.
Back to the table of contents.
Z. Alexin,
I. H. Anellis,
J. Bradfield,
M. Dam,
P. Hill,
M. R. Holmes,
A. M. Jorge,
J. Kalman,
J. Legris,
S. R. Mahaney,
B. Mayoh,
G. Mints,
J. D. Monk,
U. Nilsson,
D. Pavlovic,
L. De Raedt,
G. Semeraro,
S. Shapiro,
L. Turi,
G. Wagner,
D. S. Warren