Farewell academics talk: Colloquium Logicum 2016 – Gödel Logics

Today I had my invited talk at the Colloquium Logicum 2016, where I gave an introduction to and overview of the state of the art of Gödel Logics. Having contributed considerably to the state we are now, it was a pleasure to have the opportunity to give an invited talk on this topic.

cl16-preining

It was also somehow a strange talk (slides are available here), as it was my last as “academic”. After the rejection of extension of contract by the JAIST (foundational research, where are you going? Foreign faculty, where?) I have been unemployed – not a funny state in Japan, but also not the first time I have been, my experiences span Austrian and Italian unemployment offices. This unemployment is going to end this weekend, and after 25 years in academics I say good-bye.

Considering that I had two invited talks, one teaching assignment for the ESSLLI, submitted three articles (another two forthcoming) this year, JAIST is missing out on quite a share of achievements in their faculty database. Not my problem anymore.

It was a good time in academics, and I will surely not stop doing research, but I am looking forward to new challenges and new ways of collaboration and development. I will surely miss academics, but for now I will dedicate my energy to different things in life.

Thanks to all the colleagues who did care, and for the rest, I have already forgotten you.

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author

ESSLLI 2016 Course: Algebraic Specification and Verification with CafeOBJ

During this year’s ESSLLI (European Summer School in Logic, Language and Information) I was teaching a course on Algebraic Specification and Verification with CafeOBJ. Now that the course is over I can relax a bit and enjoy the beauty of the surrounding North Tyrol.
ESSLLI-2016-logo-darkblue-small

For those who couldn’t attend the ESSLLI or the course, here are the course materials:

Thanks to the participants for the interesting questions and participation.

What follows is the original description of the course. Continue reading

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author

CafeOBJ 1.5.5 released

Yesterday we have released CafeOBJ 1.5.5 with a long list of changes, and many more internal changes. Documentation pages have been updated with the latest reference manual (PDF, Html) as well as some new docs on CITP (in Japanese for now) and tutorials.

cafeobj-logo

To quote from our README:

CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.

Read on for changes and availability →

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author

CafeOBJ 1.5.4 released

Yesterday we have released CafeOBJ 1.5.4 with a long list of changes, and many more internal changes. Documentation pages have been updated with the latest reference manual (PDF, Html) as well as some new docs on CITP (in Japanese for now) and tutorials.

cafeobj-logo

To quote from our README:

CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.

Read on for changes and availability →

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author

Recent silence – scientific freak weeks

If you wonder why it was so silent here over the last weeks, there is a simple explanation: I am on scientific freak weeks 😉 As you might know, in my main profession I am logician, mathematician, computer scientist at the Japan Advanced Institute of Science and Technology (btw, searching urgently for a new job, in case someone is interested!!!).

purity

The last weeks have been very busy with attenting and presenting at LICS 2015 (Logic in Computer Science), followed by a workshop on Proofs as Processes organized by myself, then a presentation at CCA 2015 (Conference on Computability and Complexity in Analysis), and now working with visitors on our hyper natural deduction system. Above all that, there is also my lecture on Logical Decision Procedures at JAIST that a colleague and I a creating on the fly.

All in all a very busy July, but I hope that after the weekend, and another workshop at JAIST, things settle down around beginning of August.

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author

The Talos Principle – Solving puzzles using SAT solvers

After my last post on Portal, there was a sale of The Talos Principle, so I got it and started playing. And soon I got stuck at these kind of puzzles where one has to fit in pieces into a frame. As a logician I hate to solve something by trial and error, so I decided I write a solver for these kind of puzzles, based on a propositional logic encoding and satisfiability solver. Sometimes it is good to be logician!

Talos-Puzzles

In the Talos Principle, access to new worlds and specific items is often blocked by gates that open by putting Sigils into the frame. Of course, collecting the sigils is the most challenging part, but that is often solvable by logical thinking. On the other hand, solving these fitting puzzles drove me crazy, so let us solve them with a SAT solver. Continue reading

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author

CafeOBJ 1.5.0 released

Yesterday we have finally released CafeOBJ 1.5.0. This marks a great step forward in a long development history of this algebraic specification and verification language.

cafeobj-logo

To quote from our README:

CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.

Read on for changes and availability →

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author

Vienna Summer of Logic

This year we, the Kurt Gödel Society, are organizing the biggest event in the history of logic – the Vienna Summer of Logic. 12 conferences and many workshops, expected number of participants around 2500. Be part of it!

I have contributions to two conferences/workshops, and will be also there in my function as KGS executive member. I hope to see you all there!

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author

Gaisi Takeuti – Proof Theory

Gaisi Takeuti - Proof TheoryOne of the best works on proof theory finally is back in print – Gaisi Takeuti‘s Proof Theory. Originally published as Volume 81 in the series Studies in Logic and the Foundations of Mathematics by North-Holland, this book has been out of print for many years, and the remaining few copies were disappearing at an incredible pace. Considering that a second hand hard cover edition of this book goes for around 260USD at Amazon, the need was great for a reprint. The new edition is now published by Dover Publications, and is an exact reprint of the second edition.

As it was the book from which I learned proof theory, and together with Joseph R. Shoenfields Mathematical Logic the foundation of my logic education, I am happy to finally own my own copy of it. Now I only have to copy all the remarks and comments I scribbled into my paper copy into the new book.

Email this to someonePrint this pageShare on FacebookShare on Google+Tweet about this on TwitterShare on LinkedInFlattr the author