Thursday, June 14, 2018
Adriana Stancu (University of Bucharest)
Verification of hybrid systems using KeYmaera X
Abstract: KeYmaera X is an automated theorem prover for specifying and verifying
correctness properties of hybrid systems (systems that combine discrete and continuous dynamics).
We will present a few examples of real-life hybrid systems using differential dynamic logic
language. Then we will use KeYmaera X and its axiomatic system to check some of their properties.
The proof construction will be performed using both KeYmaera X's automated proof search engine and
by interactively applying axioms from the reduced set of differential dynamic logic axioms that
includes the first-order logic axioms and proof rules.
References:
[1] KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems
Thursday, June 7, 2018
Traian Şerbănuță (University of Bucharest)
An operational-semantics-based approach to program verification using dynamic logic
Abstract: Traditionally, program verification within modal logic, as showcased by dynamic logic,
is following the mainstream axiomatic approach proposed by Hoare/Floyd. More recently, Roșu
proposed matching logic and reachability logic as an alternative way to prove program correctness,
using directly the (executable) operational semantics of a language.
In this paper, we take first steps in exploring the amenability of dynamic logic in particular,
and of modal logic in general, to express operational semantics of languages (as axioms), and
to make use of such semantics in program verification. To do this, we use a general many-sorted polyadic modal logic which allows us to represent both the
programs and their semantics in a uniform way.
This is joint work with Ioana Leuștean.
Thursday, May 24, 2018
Mihai Prunescu (University of Bucharest and IMAR)
Continuous choice
Abstract: Generic predicates in dense orderings admit continuous choice functions.
Thursday, May 10, 2018
Traian Şerbănuță (University of Bucharest)
Foundations for Natural Proofs and Quantifier Instantiation III
Thursday, April 26, 2018
Pedro Pinto (University of Lisbon)
The bounded functional interpretation and the elimination of weak compactness
Abstract: Proof mining is a research program focused on the extraction of new quantitative
and qualitative information from proofs from ordinary results in mathematics. In the last twenty years,
proof mining has successfully been applied to results in number theory, nonlinear analysis, fixed point theory,
ergodic theory, topological dynamics, approximation theory, abstract Cauchy problems and convex optimization.
The most used proof-theoretic method is Kohlenbach’s monotone functional interpretation, a variant of Gödel’s
Dialectica where the search for precise witnesses is replaced by a search for bounds on those witnesses.
In 2005, Ferreira and Oliva introduced the bounded functional interpretation, that gives a
new interpretation of formulas and makes use of set-theoretically false principles. In recent work,
in conjunction with Fernando Ferreira and Laurențiu Leuștean,
a general principle was developed in this setting that allows the elimination of a weak sequential
compactness argument from certain types of proofs, common in fixed point theory.
The goal of this talk is twofold. First I will give a presentation of the bounded functional
interpretation in a classical setting and explain how it can be used in proof mining. Second,
I will explain this general principle and end with some first results of its application -
results by Browder, Wittmann and Bauschke.
References:
[1] F. Ferreira, P. Oliva, Bounded functional interpretation, Annals of Pure and Applied Logic 135 (2005): 73-112.
[2] F. Ferreira, Injecting uniformities into Peano arithmetic, Annals of Pure and Applied Logic 157 (2009): 122-129.
[3] U. Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics, Springer, 2008.
[4] U. Kohlenbach, On quantitative versions of theorems due to FE Browder and R. Wittmann, Advances in Mathematics 226 (2011): 2764-2795.
[5] H.H. Bauschke, The approximation of fixed points of compositions of nonexpansive mappings in Hilbert space, Journal of Mathematical Analysis
and Applications 202 (1996): 150-159.
Thursday, April 19, 2018
Cătălin Dima (Université Paris-Est Créteil)
Bisimulations for Verifying Strategic Abilities with an Application to ThreeBallot
Abstract: We propose a notion of alternating bisimulation for strategic abilities under imperfect
information. The bisimulation preserves formulas of ATL for both the objective and subjective
variants of the state-based semantics with imperfect information,
which are commonly used in the modeling and verification of
multi-agent systems. Furthermore, we apply the theoretical result to
the verification of coercion-resistance in the three-ballot voting
system, a voting protocol that does not use cryptography. In
particular, we show that natural simplifications of an initial model
of the protocol are in fact bisimulations of the original model, and
therefore satisfy the same ATL properties, including
coercion-resistance. These simplifications allow the model-checking
tool MCMAS to terminate on models with a larger number of
voters and candidates, compared with the initial model.
Joint work with Francesco Belardinelli, Rodica Bozianu, Wojtek Jamroga, Andrew Jones and Michal Knapik.
References:
[1] F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, A. V. Jones, Bisimulations for Verifying Strategic
Abilities with an Application to ThreeBallot. AAMAS 2017: 1286-1295.
Thursday, March 29, 2018
Traian Şerbănuță (University of Bucharest)
Foundations for Natural Proofs and Quantifier Instantiation II
Thursday, March 22, 2018
Traian Şerbănuță (University of Bucharest)
Foundations for Natural Proofs and Quantifier Instantiation I
Abstract: In this talk we present results from [1], explaining the efficacy of heuristics used for
dealing with quantified formulas and recursive definitions.
References:
[1] C. Löding, P. Madhusudan, L. Peña,
Foundations for Natural Proofs and Quantifier Instantiation,
Proceedings of the ACM on Programming Languages (POPL), Vol. 2, Article 10, 2018.
Thursday, March 15, 2018
Adriana Stancu (University of Bucharest)
Dynamic logic of hybrid systems
Abstract: In this talk we present differential dynamic logic, a first-order modal logic
that reasons about the behavior of hybrid systems, introduced by André Platzer [1,2,3].
References:
[1] A. Platzer, Logics of Dynamical Systems,
ACM/IEEE Symposium on Logic in Computer Science, LICS 2012,
June 25–28, 2012, Dubrovnik, Croatia, pp. 13-24.
[2] A. Platzer, Logical Analysis of Hybrid Systems:
Proving Theorems for Complex Dynamics,
Springer, 426 pages, 2010.
[3] A. Platzer, Differential Dynamic Logic for Hybrid Systems,
Journal of Automated Reasoning 41 (2008), 143-189.
Friday, March 2, 2018, 12:00
Radu Iosif (CNRS - VERIMAG, France)
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
Abstract: This paper investigates the satisfiability problem for Separation Logic,
with unrestricted nesting of separating conjunctions and implications, for prenex formulae
with quantifier prefix in the language $\exists^*\forall^*$, in the cases where the universe of possible
locations is either countably infinite or finite. In analogy with first-order logic with
uninterpreted predicates and equality, we call this fragment Bernays-Schönfinkel-Ramsey
Separation Logic [BSR(SLk)]. We show that, unlike in first-order logic, the (in)finite satisfiability
problem is undecidable for BSR(SLk) and we define two non-trivial subsets thereof, that are
decidable for finite and infinite satisfiability, respectively, by controlling the occurrences
of universally quantified variables within the scope of separating implications, as well as
the polarity of the occurrences of the latter. The decidability results are obtained by
a controlled elimination of separating connectives, described as (i) an effective
translation of a prenex form Separation Logic formula into a combination of a small
number of \emph{test formulae}, using only first-order connectives, followed by (ii) a
translation of the latter into an equisatisfiable first-order formula.
Joint work with Mnacho Echenim and Nicolas Peltier.
Thursday, February 22, 2018
Natalia Moangă (University of Bucharest)
Many-sorted polyadic modal logic
Abstract: We present our first results towards defining a many-sorted polyadic modal
logic. While the standard modal logic has only two unary operators (box and diamond), its
polyadic extension is endowed with a family of modal operators of arbitrary arities, satisfying
some appropriate identities. On top of this we can define our many-sorted version, the many-sorted
modal poyladic logic, the main difference being that the formulas (within the syntax) and the
worlds (within the semantics) are sorted sets. We will present how those changes affect the
syntax and the semantics, thus giving us the possibility to develop a new logic.
Thursday, February 8, 2018
Mircea Dumitru (University of Bucharest)
Modal logic as higher-order logic III
Thursday, January 18, 2018
Mihai Prunescu (University of Bucharest and IMAR)
First order interpretations in groups, rings and algebras II
Thursday, January 11, 2018
Mircea Dumitru (University of Bucharest)
Modal logic as higher-order logic II
Thursday, December 14, 2017
Mihai Prunescu (University of Bucharest and IMAR)
First order interpretations in groups, rings and algebras
Abstract:
We present some results of Malcev. In a first part a general method of transforming rings
in metabelian groups is recalled. In the second part we concentrate on finite dimensional
algebras over arbitrary fields and we head to the theory of all finite groups.
Thursday, December 7, 2017
Mircea Dumitru (University of Bucharest)
Modal logic as higher-order logic
Abstract:
Propositional modal logic is usually viewed as a generalization and extension of propositional classical logic.
The main argument of this paper is that a good case can be made that modal logic should be
construed as a restricted form of second order classical logic. The paper examines one aspect of
this second order connection having to do with an incompleteness phenomenon. The leading concept
is that modal incompleteness is to be explained in terms of the incompleteness of standard second order logic,
since modal language is basically a second order language.
Thursday, November 23, 2017
Marian Calborean (University of Bucharest)
Fuzzy and more. Modelling philosophical theories of vagueness on a computer
Abstract:
The debate on vagueness has been greatly enriched by the development of fuzzy logic and its
applications, many of which are computer-based. However, since such philosophical theories of
vagueness as epistemicism and super-valuationism diverge from the basic assumptions of
pluri-valuationism embedded in fuzzy logic and since, inside fuzzy theory, philosophically-potent
disagreements exist, e.g. in relation to the interpretation of logical connectives, we plan
to develop a tool for comparing theories of vagueness, each of which receive a basic tri-partite
characterization by accepted truth values, truth-functionality of connectives and valid inference rules.
Starting from a dictionary of vague sentences and using recursion, the tool can derive a
large number of propositions with their associated truth interpretations under each theory
of vagueness. The tool is to be written in common Structured Query Language (MariaDB)
with a C-like application language (PHP).
Thursday, November 16, 2017
Ioana Leuștean (University of Bucharest)
Łukasiewicz logic and MV-algebras II
Thursday, November 9, 2017
Ioana Leuștean (University of Bucharest)
Łukasiewicz logic and MV-algebras
Abstract:
After a brief introduction to Łukasiewicz logic, we focus on some specific topics connecting logic, algebra and probability theory.
Thursday, November 2, 2017
Laurențiu Leuștean (University of Bucharest and IMAR)
Proof mining in convex optimization and nonlinear analysis
Abstract:
The research program of proof mining in mathematical logic - first suggested by G. Kreisel
in the 1950s as 'unwinding of proofs' and developed by U. Kohlenbach in the 1990s and afterwards -
is a field of study that aims to analyze, using proof-theoretic tools, the proofs of
existing mathematical theorems in order to obtain their hidden quantitative content.
The new information is both of quantitative nature, such as algorithms and
effective bounds, as well as of qualitative nature, such as uniformities in the bounds.
In this talk we give an introduction to proof mining and present some recent applications in
convex optimization and nonlinear analysis.