Time: 1:00 - 2:00pm Venue: Queen Mary University of London, ITL 1st floor meeting room
Speaker: Reinhard MuskensTime: 13:00-14:00 on Tue 18/09/18Place: ITL 1st floor meeting roomHost: Mehrnoosh Sadrzadehhttp://theory.eecs.qmul.ac.uk/seminars/Abstract(Joint work with Stefan Wintein)In a now famous paper published in 1976, Nuel Belnap argues that computer reasoning should be modeled on the basis of a four-valued logic in which each value is a combination of the two classical values. Belnap also considers two lattices on these four values, one corresponding to increase in truth and non-falsity, the other to increase of information. Together these two lattices form what is now called a /bilattice/.More recently Yaroslav Shramko and Heinrich Wansing (2005) have in a sense repeated Belnap's move, arguing that the logic of the reasoning of computer /networks/ should be 16-valued, with each value corresponding to a set of Belnap's values. They consider what is called a /trilattice/ on these 16 values and distinguish between an entailment relation based on the notion of truth and one based on falsity. These two relations are not equal or each other's inverses.In this talk, which reports on joint work with Stefan Wintein, I will look at syntactic characterisations for 16-valued trilattice logics. I will show that a language with connectives for the three meet operations on the 16-element trilattice, plus three negation connectives corresponding to certain involutions on it is functionally complete (and minimally so). This language will be provided with four semantic consequence relations, one based on truth, one on falsity, one on approximation, and one the intersection of the first two. An analytic signed tableau calculus will be given that can model each of these semantic consequence relations in a sound and complete way. It has the property that a single proof in general requires several tableaux, four tableaux for any of the first three consequence relations just mentioned, and six for the last. Interpolation theorems hold for the logic on the functionally complete language, but also on many of its less expressive sublanguages. Time permitting I will also spend a few words on a simple toy theorem prover implementing the calculus (https://swish.swi-prolog.org/p/sixteentap.pl).*Directions*Queen Mary is on Mile End Road, with nearest tube stations being Stepney Green (closest one to the seminars) and Mile End. The seminars are in the Informatics Teaching Laboratory, floor 1: https://goo.gl/maps/hYgvAwTx76vAs the building has card access, it is best to inform us that you will be coming (nikos.tzevelekos@qmul.ac.uk).