The Experts below are selected from a list of 78 Experts worldwide ranked by ideXlab platform
Deepak Kapur - One of the best experts on this subject based on the ideXlab platform.
-
Interpolation and Amalgamation for Arrays with MaxDiff
Lecture Notes in Computer Science, 2021Co-Authors: Silvio Ghilardi, Alessandro Gianola, Deepak KapurAbstract:AbstractIn this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the Extensionality Axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.
-
Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version).
arXiv: Logic in Computer Science, 2020Co-Authors: Silvio Ghilardi, Alessandro Gianola, Deepak KapurAbstract:We enrich the McCarthy theory of arrays with a maxdiff operation (this operation returns the biggest index where two given arrays differ). It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the Extensionality Axiom). Our maxdiff operation significantly increases the level of expressivity (for instance, it allows the definition of a length function); however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results in this paper, via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and we show how to convert them into concrete interpolation algorithms via a hierarchical approach.
Silvio Ghilardi - One of the best experts on this subject based on the ideXlab platform.
-
Interpolation and Amalgamation for Arrays with MaxDiff
Lecture Notes in Computer Science, 2021Co-Authors: Silvio Ghilardi, Alessandro Gianola, Deepak KapurAbstract:AbstractIn this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the Extensionality Axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.
-
Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version).
arXiv: Logic in Computer Science, 2020Co-Authors: Silvio Ghilardi, Alessandro Gianola, Deepak KapurAbstract:We enrich the McCarthy theory of arrays with a maxdiff operation (this operation returns the biggest index where two given arrays differ). It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the Extensionality Axiom). Our maxdiff operation significantly increases the level of expressivity (for instance, it allows the definition of a length function); however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results in this paper, via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and we show how to convert them into concrete interpolation algorithms via a hierarchical approach.
Alessandro Gianola - One of the best experts on this subject based on the ideXlab platform.
-
Interpolation and Amalgamation for Arrays with MaxDiff
Lecture Notes in Computer Science, 2021Co-Authors: Silvio Ghilardi, Alessandro Gianola, Deepak KapurAbstract:AbstractIn this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the Extensionality Axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.
-
Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version).
arXiv: Logic in Computer Science, 2020Co-Authors: Silvio Ghilardi, Alessandro Gianola, Deepak KapurAbstract:We enrich the McCarthy theory of arrays with a maxdiff operation (this operation returns the biggest index where two given arrays differ). It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the Extensionality Axiom). Our maxdiff operation significantly increases the level of expressivity (for instance, it allows the definition of a length function); however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results in this paper, via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and we show how to convert them into concrete interpolation algorithms via a hierarchical approach.
Eugenio G. Omodeo - One of the best experts on this subject based on the ideXlab platform.
-
Decidability Results for Sets with Atoms ∗
2008Co-Authors: Agostino Dovier, Andrea Formisano, Eugenio G. OmodeoAbstract:Formal Set Theory is traditionally concerned with pure sets; consequently, the satisfiability problem for fragments of set theory was most often addressed (and in many cases positively solved) in the pure framework. In practical applications, however, it is common to assume the existence of a number of primitive objects (sometimes called atoms) that can be members of sets but behave differently from them. If these entities are assumed to be devoid of members, the standard Extensionality Axiom must be revised; then decidability results can sometimes be achieved via reduction to the pure case and sometimes can be based on direct goal-driven algorithms. An alternative approach to modeling atoms, that allows one to retain the original formulation of Extensionality, was proposed by Quine: atoms are self-singletons. In this paper we adopt this approach in coping with the satisfiability problem: we show the decidability of this problem relativized to ∃ ∗ ∀-sentences, and develop a goal-driven unification algorithm
-
Decidability results for sets with atoms
ACM Transactions on Computational Logic, 2006Co-Authors: Agostino Dovier, Andrea Formisano, Eugenio G. OmodeoAbstract:Formal set theory is traditionally concerned with pure sets; consequently, the satisfiability problem for fragments of set theory was most often addressed (and in many cases positively solved) in the pure framework. In practical applications, however, it is common to assume the existence of a number of primitive objects (sometimes called atoms) that can be members of sets but behave differently from them. If these entities are assumed to be devoid of members, the standard Extensionality Axiom must be revised; then decidability results can sometimes be achieved via reduction to the pure case and sometimes can be based on direct goal-driven algorithms. An alternative approach to modeling atoms that allows one to retain the original formulation of Extensionality was proposed by Quine: atoms are self-singletons. In this article we adopt this approach in coping with the satisfiability problem: We show the decidability of this problem relativized to ∃*∀-sentences, and develop a goal-driven unification algorithm.
-
APPIA-GULP-PRODE - Decidability results for sets with atoms.
2001Co-Authors: Agostino Dovier, Andrea Formisano, Eugenio G. OmodeoAbstract:Formal set theory is traditionally concerned with pure sets; consequently, the satisfiability problem for fragments of set theory was most often addressed (and in many cases positively solved) in the pure framework. In practical applications, however, it is common to assume the existence of a number of primitive objects (sometimes called atoms) that can be members of sets but behave differently from them. If these entities are assumed to be devoid of members, the standard Extensionality Axiom must be revised; then decidability results can sometimes be achieved via reduction to the pure case and sometimes can be based on direct goal-driven algorithms. An alternative approach to modeling atoms that allows one to retain the original formulation of Extensionality was proposed by Quine: atoms are self-singletons. In this article we adopt this approach in coping with the satisfiability problem: We show the decidability of this problem relativized to ∃*∀-sentences, and develop a goal-driven unification algorithm.
Zoltan Molnar - One of the best experts on this subject based on the ideXlab platform.
-
Induced Cylindric Algebras of Choice Structures
arXiv: Logic, 2011Co-Authors: Zoltan MolnarAbstract:One of the benefit properties implied by the Extensionality Axiom of Hilbert's epsilon calculus is that the calculus becomes complete with respect to the choice structures as semantics. Another implication of the Axiom, discussed in the paper, is that an algebra is induced over the universe of the canonical model of a theory, which is isomorphic to a quotient algebra of the Lindenbaum--Tarski algebra of the theory. Especially, in the case of Boolean or monadic algebras, the canonical model of the theory of a sigma complete model is isomorphic to the algebra induced by the Axiom of Extensionality.
