Modalities 〈ψ〉 with ψ a first order formula
A modal formula of the form 〈R〉 can be seen, through the standard translation into FO as (∃y)(Rxy ∧ STy(ψ)). We can think that the relation R as a formula Rxy with two free variables. We can generalize this idea to an arbitrary formula with n+1 free variables defining an n ary modality. Explore the model theory of this family of languages.
Binders weaker than ↓
Can we define weaker, decidable versions of ↓? Why is ↓ so expressive? Can we use the presentation of Marx & Venema of the classical cuantifiers as modal operators, do the same for ↓, and see if we also get a "weak" version of ↓?
Binders over weak logics
Decidability of Hybrid Categorial Type Logic. The basic language is NP-complete, and one would guess it is still decidable when ↓ is added. Also there are a number of interesting issues here. What is exacly the expressive power of this logic?
A Herbrand theorem for hybrid logics
We know that we can define the diagram of a model in H(@), and this is usually a precondition for the proof of some version of the Herbrand Theorem. How far can we go in H(@)? What is the difference with the Herbrand Theorem proved by Fitting for ML, where the diagram cannot be defined?
Lindstrom Lemma for PDL
Investigate a Lindstrom theorem for PDL, extending the original result of Maarten de Rijke. Think of the new ideas in Johan's proof.
Bisimulations for Description Logics
Two level bisimulation for Description Logics.
Dynamic clause selection in HyLoRes
The selection funcion in HyLoRes is, at the moment, static. It is fixed via parameters when the prover is invoqued. It would be posible to define this function dynamically during the computation of new clauses. What is the proper way of doing this?
An efficient way to compute the order relationship between HyLoRes formulas
Improve the complexity of the algorithm to compute order between formulas in HyLoRes.
Use MPI (Message Passing Interface) to obtain a paralel and distributed version of HyLoRes.
Adding state to HyLoRes
Add a notion of state to HyLoRes, so that recomputing the redundand part of the saturation of a given theory is not necessary anymore.
Using Description Logics in edos-project
In a previous project a propositional prover was used to codify the dependencies between packages in a linux distribution and check, for example, for inconsistencies. As the model that needs to be encoded is about packages and dependencies bewteen packages it makes sense to use DL as a more expressive language.
A system for model maintenance
Investigate the trade-off between a model checker and a theorem prover to mantain a model that satisfies certain properties.
Horn clauses for H(@)
Investigate the proper notion of Horn Clauses for H(@).
A short demonstration extractor from HyLoRes demonstrations
Given a HyLoRes demonstration, the idea is to develop a procedure to extract a minimal demonstration for the same theorem.
A random generator for hybrid formulas
Investigate the generation of hybrid random formulas to be able to produce appropriate sets of formulas to make tests, given a set of parameters.
Using HyLoRes for consistence verification in a temporal discourse
Automatically represent a temporal discourse in (restricted) natural language with a hybrid formula, and use HyLoRes to check temporal consistency.