Decision procedures for elementary sublanguages of set theory: XII. Multilevel syllogistic extended with singleton and choice operators

Completeness results and decision algorithms for unquantified theory of sets involving the choice operator are presented. The interest for considering the choice operator is justified by the problem of formalizing transfinite induction in automated theorem proving.     

On the decidability of sparse univariate polynomial interpolation

We consider the problem of determining whether or not there exists a sparse univariate polynomial that interpolates a given setS={(x _i ,y _i )} of points. Several important cases are resolved, e.g., the case when thex _i's are all positive rational numbers. But the general problem remains open.     

Refining the Undecidability Border of Weak Bisimilarity

Weak bisimilarity is one of the most studied behavioural equivalences. This equivalence is undecidable for pushdown processes (PDA), process algebras (PA), and multiset automata (MSA, also known as parallel pushdown processes, PPDA). Its decidability is an open question for basic process algebras (BPA) and basic parallel processes (BPP). We move the undecidability border towards these classes by showing that the equivalence remains undecidable for weakly extended versions of BPA and BPP. In fact, we show that the weak bisimulation equivalence problem is undecidable even for normed subclasses of BPA and BPP extended with a finite constraint system.     

T-Resolution: Refinements and Model Elimination

T-resolution is a binary rule, proposed by Policriti and Schwartz in 1995 for theorem proving in first-order theories (T-theorem proving) that can be seen – at least at the ground level – as a variant of Stickel's theory resolution. In this paper we consider refinements of this rule as well as the model elimination variant of it. After a general discussion concerning our viewpoint on theorem proving in first-order theories and a brief comparison with theory resolution, the power and generality of T-resolution are emphasized by introducing suitable linear and ordered refinements, uniformly and in strict analogy with the standard resolution approach. Then a model elimination variant of T-resolution is introduced and proved to be sound and complete; some experimental results are also reported. In the last part of the paper we present two applications of T-resolution: to constraint logic programming and to modal logic.     

A Logic with Relative Knowledge Operators

We study a knowledge logic that assumes that to each set of agents, an indiscernibility relation is associated and the agents decide the membership of objects or states up to this indiscernibility relation. Its language contains a family of relative knowledge operators. We prove the decidability of the satisfiability problem, we show its EXPTIME-completeness and as a side-effect, we define a complete Hilbert-style axiomatization.