Integrated Formal Methods - Méry, Dominique; Merz, Stephan
This volume contains the proceedings of iFM 2010, the 8th International Conference on Integrated Formal Methods. The conference took place during October 12-14, 2010, at the INRIA research center and the LORIA laboratory in Nancy, France. Previous editions were held in York, Dagstuhl, Turku, Canter- bury, Eindhoven, Oxford, and Düsseldorf. The iFM conference series seeks to promote research into the combination of different formal methods, and of formal and semi-formal methods, for system development. Such combinations are useful in order to apprehend different aspects of systems, including functional correctness, security, performance, and fault-tolerance. The conference provides a forum for discussing...
Topological semantics for hybrid logic - Sustretov, Dmitry
Ph.D. in Computer Science, INRIA Nancy Grand Est, projet TALARIS/Université Henri Poincaré, Nancy, France. Under supervision of Patrick Blackburn.
Physics and Proof Theory - Woltzenlogel Paleo, Bruno
Axiomatization of Physics (and Science in general) has many drawbacks that are correctly criticized by opposing philosophical views of Science. This paper shows that, by giving formal proofs a more promi- nent role in the formalization, many of the drawbacks can be solved and many of the opposing views are naturally conciliated. Moreover, this ap- proach allows, by means of Proof Theory, to open new conceptual bridges between the disciplines of Physics and Computer Science.
Proof Compression with the CIRes Method [Abstract] - Woltzenlogel Paleo, Bruno
It is well-known that eliminating cuts from sequent calculus proofs frequently increases the size and length of proofs. In the worst case, cut-elimination can produce non-elementarily larger and longer proofs [3, 2]. Given this fact, it is natural to attempt to devise methods that could introduce cuts and compress cut-free proofs. However, this has been a notoriously difficult task. Indeed, the problem of answering, given a proof φ and a number l such that l ≤ length(φ), whether there is a proof ψ (possibly with cuts) of the same theorem and such that length(ψ) < l is known to be...
Special Issue on Hybrid Logics - Areces, Carlos; Blackburn, Patrick
Special Issue of the Journal of Applied Logic. C. Areces and P. Blackburn (editors).
Some Remarks on Relations between Proofs and Games - Galmiche, Didier; Larchey-Wendling, Dominique; Vidal-Rosset, Joseph
This paper aims at studying relations between proof systems and games in a given logic and at analyzing what can be the interest and limits of a game formulation as an alternative semantic framework for modeling proof search and also for understanding relations between logics. In this perspective, we rstly study proofs and games at an abstract level which is neither related to a particular logic nor adopts a speci c focus on their relations. Then, in order to instantiate such an analysis, we describe a dialogue game for intuitionistic logic and emphasize the adequateness between proofs and winning strategies...