GLyC - Logic, Language and Computability Research Group

Theoretical topics. [Back to index]

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.

Practical topics. [Back to index]

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.

HyLoRes paralelization

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.

Mixed topics. [Back to index]

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.