EDBT 2026 Demo / reviewers in the wild / expert
Andrea Formisano 0001
dblp:50/3517-1
· DBLP profile ↗
44ranked-venue papers
5as first author
14since 2021 · last 2025
0000-0002-6755-9314ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 25 · 3 first-author · 6 since 2021Artificial intelligence and machine learning · 14 · 1 first-author · 5 since 2021Software engineering, systems software and programming languages · 12 · 5 since 2021Graphics, computer vision, multimedia, augmented reality and games · 3 · 1 since 2021Systems, architecture and hardware · 1 · 1 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | A Prototyping Framework for Reduct-Based ELP Solvers: Methodology and ImplementationabstractEpistemic Logic Programs (ELPs) extend Answer Set Programming (ASP) by incorporating epistemic operators, notably the knowledge operator K. The semantics of ELPs are defined through the concept of world views, which are sets that, in turn, comprise sets of atoms. Various semantic frameworks have been proposed, many of which, including influential early approaches, are based on reduct-based definitions. These approaches generalize the ASP methodology to ELPs by selecting a candidate world view, constructing the corresponding reduct of the program based on this candidate, computing the stable models of this reduct, and subsequently verifying if the initial candidate is indeed a world view. While specialized inference engines (ELP solvers) have been developed for certain semantic approaches, there remains no consensus regarding the “correct” semantics for ELPs, and new or variant semantics continue to emerge. In response to this evolving situation, this paper introduces a novel fast prototyping methodology that enables the implementation of solvers for any reduct-based semantics. The main advantage of this approach is the ability to rapidly experiment with new semantics on small- to medium-sized programs, as opposed to the very limited small-scale experimentation seen in the literature. This facilitates a thorough preliminary evaluation prior to committing to the more resource-intensive development of dedicated solvers. As a concrete demonstration, we apply our methodology to seminal semantic frameworks already established in the literature. Nevertheless, our approach is readily adaptable to accommodate other reduct-based semantics. Stefania Costantini, Andrea Formisano 0001 |
ECAI | 2 |
| 2025 | GPU Accelerated Compact-Table PropagationabstractAbstract Constraint Programming developed within Logic Programming in the Eighties; nowadays all Prolog systems encompass modules capable of handling constraint programming on finite domains demanding their solution to a constraint solver. This work focuses on a specific form of constraint, the so-called table constraint, used to specify conditions on the values of variables as an enumeration of alternative options. Since every condition on a set of finite domain variables can be ultimately expressed as a finite set of cases, Table can, in principle, simulate any other constraint. These characteristics make Table one of the most studied constraints ever, leading to a series of increasingly efficient propagation algorithms. Despite this, it is not uncommon to encounter real-world problems with hundreds or thousands of valid cases that are simply too many to be handled effectively with standard CPU-based approaches. In this paper, we deal with the Compact-Table (CT) algorithm, the state-of-the-art propagation algorithms for Table. We describe how CT can be enhanced by exploiting the massive computational power offered by modern Graphics Processing Units (GPUs) to handle large Table constraints. In particular, we report on the design and implementation of GPU-accelerated CT, on its integration into an existing constraint solver, and on an experimental validation performed on a significant set of instances. Enrico Santi, Agostino Dovier, Andrea Formisano 0001, Fabio Tardivo |
Theory Pract. Log. Program. | 3 |
| 2024 | Towards Explainable Weather Forecasting Through FastLAS
Talissa Dreossi, Agostino Dovier, Andrea Formisano 0001, Mark Law, Agostino Manzato, Alessandra Russo, Matthew Tait |
LPNMR | 3 |
| 2024 | Advances in Computational Logic (CILC23): PrefaceabstractThis special issue of The Journal of Logic and Computation contains the revised and improved versions of selected papers presented at CILC-2023, the 38th Italian Conference on Computational Logic, which took place in Udine, Italy, from 21 to 23 June 2023. The Italian Association for Logic Programming (GULP) and the Department of Mathematics, Informatics and Physics of the University of Udine collaborated to organize this event. The yearly conferences of the Italian Association of Logic Programming, starting from 1986, have consistently offered valuable and inspiring opportunities for national and international researchers to share scientific findings, discuss ideas and suggest novel initiatives and projects in the field of Computational Logic. The continuous achievements of these conferences demonstrate the lively condition of a productive research field that addresses the theoretical foundations of logic programming and computational logics, the implementation techniques of logic programming languages and automated reasoning systems and the practical applications of the field. Agostino Dovier, Andrea Formisano 0001 |
J. Log. Comput. | 2 |
| 2024 | Epistemic Logic Programs: A Study of Some PropertiesabstractAbstract Epistemic logic programs (ELPs), extend answer set programming (ASP) with epistemic operators. The semantics of such programs is provided in terms of world views, which are sets of belief sets, that is, syntactically, sets of sets of atoms. Different semantic approaches propose different characterizations of world views. Recent work has introduced semantic properties that should be met by any semantics for ELPs, like the Epistemic Splitting Property, that, if satisfied, allows to modularly compute world views in a bottom-up fashion, analogously to “traditional” ASP. We analyze the possibility of changing the perspective, shifting from a bottom-up to a top-down approach to splitting. We propose a basic top-down approach, which we prove to be equivalent to the bottom-up one. We then propose an extended approach, where our new definition: (i) is provably applicable to many of the existing semantics; (ii) operates similarly to “traditional” ASP; (iii) provably coincides under any semantics with the bottom-up notion of splitting at least on the class of Epistemically Stratified Programs (which are, intuitively, those where the use of epistemic operators is stratified); (iv) better adheres to common ASP programming methodology. Stefania Costantini, Andrea Formisano 0001 |
Theory Pract. Log. Program. | 2 |
| 2023 | Constraint Propagation on GPU: A Case Study for the Cumulative Constraint
Fabio Tardivo, Agostino Dovier, Andrea Formisano 0001, Laurent D. Michel, Enrico Pontelli |
CPAIOR | 3 |
| 2023 | Constraint propagation on GPU: A case study for the AllDifferent constraintabstractAbstract The AllDifferent constraint is a fundamental tool in Constraint Programming. It naturally arises in many problems, from puzzles to scheduling and routing applications. Such popularity has prompted an extensive literature on filtering and propagation for this constraint. This paper investigates the use of General Processing Units (GPUs) to accelerate filtering and propagation. In particular, the paper presents an efficient parallelization of the AllDifferent constraint on GPU, along with an analysis of different design and implementation choices and evaluation of the performance of the resulting system on several benchmarks. Fabio Tardivo, Agostino Dovier, Andrea Formisano 0001, Laurent D. Michel, Enrico Pontelli |
J. Log. Comput. | 3 |
| 2022 | Epistemic Logic Programs: A Study of Some Properties
Stefania Costantini, Andrea Formisano 0001 |
LPNMR | 2 |
| 2022 | Parallel Logic Programming: A SequelabstractAbstract Multi-core and highly connected architectures have become ubiquitous, and this has brought renewed interest in language-based approaches to the exploitation of parallelism. Since its inception, logic programming has been recognized as a programming paradigm with great potential for automated exploitation of parallelism. The comprehensive survey of the first twenty years of research in parallel logic programming, published in 2001, has served since as a fundamental reference to researchers and developers. The contents are quite valid today, but at the same time the field has continued evolving at a fast pace in the years that have followed. Many of these achievements and ongoing research have been driven by the rapid pace of technological innovation, that has led to advances such as very large clusters, the wide diffusion of multi-core processors, the game-changing role of general-purpose graphic processing units, and the ubiquitous adoption of cloud computing. This has been paralleled by significant advances within logic programming, such as tabling, more powerful static analysis and verification, the rapid growth of Answer Set Programming, and in general, more mature implementations and systems. This survey provides a review of the research in parallel logic programming covering the period since 2001, thus providing a natural continuation of the previous survey. In order to keep the survey self-contained, it restricts its attention to parallelization of the major logic programming languages (Prolog, Datalog, Answer Set Programming) and with an emphasis on automated parallelization and preservation of the sequential observable semantics of such languages. The goal of the survey is to serve not only as a reference for researchers and developers of logic programming systems but also as engaging reading for anyone interested in logic and as a useful source for researchers in parallel systems outside logic programming. Agostino Dovier, Andrea Formisano 0001, Gopal Gupta 0001, Manuel V. Hermenegildo, Enrico Pontelli, Ricardo Rocha 0001 |
Theory Pract. Log. Program. | 2 |
| 2021 | An Epistemic Logic for Multi-agent Systems with Budget and Costs
Stefania Costantini, Andrea Formisano 0001, Valentina Pitoni |
JELIA | 2 |
| 2021 | Adding Metalogic Features to Knowledge Representation LanguagesabstractIn this paper we present a methodology for introducing customizable metalogic features in logic-based knowledge representation and reasoning languages. The proposed approach is based on concepts of introspection and reflection previously introduced and discussed by various authors in relevant literature. This allows a knowledge engineer to specify enhanced reasoning engines by defining properties and meta-properties of relations as expressible for instance in OWL. We employ meta-level axiom schemata based upon a naming (reification) device. We propose general principles for extending the semantics of “host” formalisms accordingly. Consequently, suitable pre-defined libraries of properties can be made available, while user-defined new schemata are also allowed. We make the specific cases of Answer Set Programming (ASP) and Datalog±, where such features may be part of software engineering toolkits for these programming paradigms. On the one hand, concerning ASP, we extend the programming principles and practice to accommodate the proposed methodology, so as to perform meta-reasoning within the plain ASP semantics. The computational complexity of the resulting framework does not change. On the other hand, we show how metalogic features can significantly enrich Datalog± with minor changes to its operational semantics (provided in terms of “chase”) and, also in this case, no additional complexity burden. Stefania Costantini, Andrea Formisano 0001 |
Fundam. Informaticae | 2 |
| 2021 | Scalable Energy Games Solvers on GPUsabstractModeling the consumption of limited resources, e.g., time or energy, plays a central role on the design of reactive systems such as embedded controllers. To this aim, quantitative objectives are defined on game arenas that can be easily modeled as weighted graphs. Instances of these games, calledenergy games, can be solved in${\mathcal {O}(\vert {E}\vert {\cdot }\vert {V}\vert {\cdot }W)}$where$W$is the maximum weight. Recent work has demonstrated that sequential implementations hardly solve practical instances due to their size and the number of interactions required to converge to a solution. Recent work has demonstrated that sequential implementations hardly solve practical instances. Furthermore, emerging approaches, that have investigated the parallelism of CPUs multi-core and GPU for solving theinitial credit problemfor energy games, still perform poorly due to the non-trivial characteristics of these graphs. In this article we first describe a revised version of the algorithm on multi-core CPU that obtains a faster convergence time on real-world graphs with up to 30x against the serial implementation by showing good scalability overall. Second, we provide a new GPU-based parallel implementation based on warp-level primitives that allows to reduce the time-to-solution on several instances with up to 3.6x of speed-up against traditional parallel vertex-based approaches. We also discuss a methodology to build synthetic energy games to validate the scalability of parallel algorithms on two totally different settings. Andrea Formisano 0001, Raffaella Gentilini, Flavio Vella |
IEEE Trans. Parallel Distributed Syst. | 1 |
| 2021 | Introduction to the 37th International Conference on Logic Programming Special Issue I
Alex Brik, Andrea Formisano 0001, Yanhong A. Liu, Joost Vennekens |
Theory Pract. Log. Program. | 2 |
| 2021 | Introduction to the 37th International Conference on Logic Programming Special Issue II
Alex Brik, Andrea Formisano 0001, Yanhong A. Liu, Joost Vennekens |
Theory Pract. Log. Program. | 2 |
| 2019 | Introduction to the 35th International Conference on Logic Programming Special Issue
Esra Erdem 0001, Andrea Formisano 0001, Germán Vidal, Fangkai Yang |
Theory Pract. Log. Program. | 2 |
| 2018 | 23rd RCRA International workshop on "Experimental evaluation of algorithms for solving problems with combinatorial explosion"abstract"23rd RCRA International workshop on “Experimental evaluation of algorithms for solving problems with combinatorial explosion”." Journal of Experimental & Theoretical Artificial Intelligence, 30(4), pp. 479–480 Stefano Bistarelli, Andrea Formisano 0001, Marco Maratea |
J. Exp. Theor. Artif. Intell. | 2 |
| 2016 | Multi-Context Systems in TimeabstractIn this paper we consider how to enhance flexibility and generality in Multi-Context Systems (MCS) by considering that contexts can evolve over time, that bridge-rule application can be proactive (according to a context's specific choice), and not instantaneous but requiring an execution mechanism. We introduce bridge-rule patterns to make bridge-rules parametric w.r.t. the involved contexts. Stefania Costantini, Andrea Formisano 0001 |
ECAI | 2 |
| 2016 | A GPU Implementation of the ASP Computation
Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli, Flavio Vella |
PADL | 2 |
| 2016 | PrefaceabstractThis special issue of Fundamenta Informaticae publishes extended and revised versions of the best papers orally presented at the 22nd RCRA International Workshop (RCRA 2015). 1 This event follows the series of the RCRA (the working group of the AI*IA association on Knowledge Representation and Automated Reasoning) annual meetings, held since 1994, and that from 2007 became an international workshop.RCRA 2015 was held in Ferrara, Italy, on 22 September 2015 as a satellite workshop of the 14th Conference of the Italian Association for Artificial Intelligence (AI*IA 2015).The success of all these events shows that RCRA is nowadays established as a major forum for exchanging ideas and proposing experimentation methodologies for algorithms in Artificial Intelligence. Stefano Bistarelli, Andrea Formisano 0001, Marco Maratea, Paolo Torroni |
Fundam. Informaticae | 2 |
| 2016 | Theoretical Computer Science in Italy
Stefano Bistarelli, Andrea Formisano 0001 |
Theor. Comput. Sci. | 2 |
| 2016 | Query answering in resource-based answer set semanticsabstractAbstract In recent work we defined resource-based answer set semantics, which is an extension to answer set semantics stemming from the study of its relationship with linear logic. In fact, the name of the new semantics comes from the fact that in the linear-logic formulation every literal (including negative ones) were considered as a resource. In this paper, we propose a query-answering procedure reminiscent of Prolog for answer set programs under this extended semantics as an extension of XSB-resolution for logic programs with negation.1We prove formal properties of the proposed procedure. Under consideration for acceptance in TPLP. Stefania Costantini, Andrea Formisano 0001 |
Theory Pract. Log. Program. | 2 |
| 2015 | Negation as a Resource: a Novel View on Answer Set SemanticsabstractIn recent work, we provided a formulation of ASP programs in terms of linear logic theories. Answer sets were characterized in terms of maximal tensor conjunctions provable from such theories. In this paper, we propose a full comparison between Answer Set Semantics and its variation obtained by int erpreting literals (including negative literals) as resources, which leads to a different interpretation of negation. We argue that this novel view can be of both theoretical and practical interest, and we propose a modified Answer Set Semantics that we call Resource-based Answer Set Semantics. An advantage is that of avoiding inconsistencies, as every program has a (possibly empty) resource-based answer set. This implies however the introduction of a different way of representing constraints. We provide a characterization of the new semantics as a variation of the answer set semantics, and also in terms of Autoepistemic Logic. The latter characterization leads to a way of computing resource-based answer set via answer set solvers. Stefania Costantini, Andrea Formisano 0001 |
Fundam. Informaticae | 2 |
| 2015 | CUD@SAT: SAT solving on GPUsabstractThe parallel computing power offered by graphic processing units (GPUs) has been recently exploited to support general purpose applications – by exploiting the availability of general API and the single-instruction multiple-thread-style parallelism present in several classes of problems (e.g. numerical simulations and matrix manipulations) – where relatively simple computations need to be applied to all items in large sets of data. This paper investigates the use of GPUs in parallelising a class of search problems, where the combinatorial nature leads to large parallel tasks and relatively less natural symmetries. Specifically, the investigation focuses on the well-known satisfiability testing (SAT) problem and on the use of the NVIDIA compute unified device architecture, one of the most popular platforms for GPU computing. The paper explores ways to identify strong sources of GPU-style parallelism from SAT solving. The paper describes experiments with different design choices and evaluates the results. The outcomes demonstrate the potential for this approach, leading to one order of magnitude of speedup using a simple NVIDIA platform. Alessandro Dal Palù, Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
J. Exp. Theor. Artif. Intell. | 3 |
| 2013 | Negation as a Resource: A Novel View on Answer Set Semantics
Stefania Costantini, Andrea Formisano 0001 |
LPNMR | 2 |
| 2013 | Product and Production Process Modeling and ConfigurationabstractProduct configuration systems are an emerging technology that supports companies in deploying mass customization strategies. Such strategies need to cover the management of the whole customizable product cycle. Adding process modeling and configuration features to a product configurator may improve its ability to assist mass customization development. In this paper, we describe a modeling framework, PRODPROC, that allows one to model both a product and its production process. We first introduce our framework by describing how configurable products are modeled. Then, we describe the main features and capabilities offered to model production processes and to link them with the corresponding products models. The configuration task (namely, the procedure that, from a configurable object/activity generates a configured product/process) is then analyzed. We also outline a possible CSP-based implementation of a configurator. A comparison with some of the existing systems for product configuration and process modeling emphasizes that none of the considered system/tools offers the complete set of features supported by PRODPROC for interdependent product and process modeling/configuration. Dario Campagna, Andrea Formisano 0001 |
Fundam. Informaticae | 2 |
| 2013 | Nested Weight Constraints in ASPabstractWeight constraints are a powerful programming construct that has proved very useful within the Answer Set Programming paradigm. In this paper, we argue that practical Answer Set Programming might take profit from introducing some forms of nested weight constraints. We define such empowered constraints (that we call “Nested Weight Constraints”) and discuss their semantics and their complexity. Stefania Costantini, Andrea Formisano 0001 |
Fundam. Informaticae | 2 |
| 2013 | Autonomous agents coordination: Action languages meet CLP() and LindaabstractAbstract The paper presents a knowledge representation formalism, in the form of a high-levelAction Description Language (ADL)for multi-agent systems, where autonomous agents reason and act in a shared environment. Agents are autonomously pursuing individual goals, but are capable of interacting through a shared knowledge repository. In their interactions through shared portions of the world, the agents deal with problems of synchronization and concurrency; the action language allows the description of strategies to ensure a consistent global execution of the agents’ autonomously derived plans. A distributed planning problem is formalized by providing the declarative specifications of the portion of the problem pertaining to a single agent. Each of these specifications is executable by a stand-alone CLP-based planner. The coordination among agents exploits a Linda infrastructure. The proposal is validated in a prototype implementation developed in SICStus Prolog. Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
Theory Pract. Log. Program. | 2 |
| 2011 | Weight Constraints with Preferences in ASP
Stefania Costantini, Andrea Formisano 0001 |
LPNMR | 2 |
| 2010 | Extending and Implementing RASPabstractIn previous work we have proposed an extension to ASP (Answer Set Programming), called RASP, standing for ASP with Resources. RASP supports declarative reasoning on production and consumption of (amounts of) resources. The approach combines answer se Stefania Costantini, Andrea Formisano 0001, Davide Petturiti |
Fundam. Informaticae | 2 |
| 2010 | An Investigation of Multi-Agent Planning in CLPabstractThis paper explores the use of Constraint Logic Programming (CLP) as a platform for experimenting with planning problems in the presence of multiple interacting agents. The paper develops a novel constraint-based action language, ℬMAP , that enables Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
Fundam. Informaticae | 2 |
| 2010 | Answer Set Programming with ResourcesabstractIn this paper, we propose an extension of Answer Set Programming (ASP) to support declarative reasoning on consumption and production of resources. We call the proposed extension RASP, standing for “Re-sourced ASP”. Resources are modeled by introducing special atoms, called amount-atoms, to which we associate quantities that represent the avail-able amount of a certain resource. The “firing ” of a RASP-rule involving amount-atoms can both consume and produce resources. A RASP-rule can be fired several times, according to its definition and to the avail-able quantities of required resources. We define the semantics for RASP programs by extending the usual answer set semantics. Different answer sets correspond to different possible allocations of available resources. We then propose an implementation based on standard ASP-solvers. The im-plementation consists of a standard translation of each RASP-rule into a set of plain ASP rules and of an inference engine that manages the firing of RASP-rules. Key words: Answer set programming, non-monotonic logic program- Stefania Costantini, Andrea Formisano 0001 |
J. Log. Comput. | 2 |
| 2010 | Multivalued action languages with constraints in CLP(FD)abstractAbstract Action description languages, such as and ℬ (Gelfond and Lifschitz,Electronic Transactions on Artificial Intelligence, 1998, vol. 2, pp. 193—210), are expressive instruments introduced for formalizing planning domains and planning problem instances. The paper starts by proposing a methodology to encode an action language (with conditional effects and static causal laws), a slight variation of ℬ, usingConstraint Logic Programming over Finite Domains. The approach is then generalized to raise the use of constraints to the level of the action language itself. A prototype implementation has been developed, and the preliminary results are presented and discussed. Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
Theory Pract. Log. Program. | 2 |
| 2009 | Representing Multi-agent Planning in CLP
Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
LPNMR | 2 |
| 2009 | An empirical study of constraint logic programming and answer set programming solutions of combinatorial problemsabstractThis paper presents experimental comparisons between the declarative encodings of various computationally hard problems in Answer Set Programming (ASP) and Constraint Logic Programming over Finite Domains (CLP(FD)). The objective is to investigate how solvers in the two domains respond to different problems, highlighting the strengths and weaknesses of their implementations, and suggesting criteria for choosing one approach over the other. Ultimately, the work in this paper is expected to lay the foundations for a transfer of technology between the two domains, for example by suggesting ways to use CLP(FD) in the execution of ASP. Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
J. Exp. Theor. Artif. Intell. | 2 |
| 2008 | Comparative uncertainty: theory and automationabstractIn recent decades, qualitative approaches to probabilistic uncertainty have received more and more attention. We propose a characterisation of partial preference orders through a uniform axiomatic treatment of a variety of qualitative uncertainty notions. To this end, we prove a representation result that connects qualitative notions of partial uncertainty to their numerical counterparts. We describe an executable specification, in the declarative framework of Answer Set Programming, that constitutes the core engine for qualitative management of uncertainty. Some basic reasoning tasks are also identified. Andrea Capotorti, Andrea Formisano 0001 |
Math. Struct. Comput. Sci. | 2 |
| 2007 | An Experimental Comparison of Constraint Logic Programming and Answer Set Programming
Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
AAAI | 2 |
| 2007 | Multivalued Action Languages with Constraints in CLP(FD)
Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
ICLP | 2 |
| 2006 | Decidability results for sets with atomsabstractFormal 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. Agostino Dovier, Andrea Formisano 0001, Eugenio G. Omodeo |
ACM Trans. Comput. Log. | 2 |
| 2005 | A Comparison of CLP(FD) and ASP Solutions to NP-Complete Problems
Agostino Dovier, Andrea Formisano 0001, Enrico Pontelli |
ICLP | 2 |
| 2005 | The axiom of elementary sets on the edge of Peircean expressibilityabstractAbstract Being able to state the principles which lie deepest in the foundations of mathematics by sentences in three variables is crucially important for a satisfactory equational rendering of set theories along the lines proposed by Alfred Tarski and Steven Givant in their monograph of 1987. The main achievement of this paper is the proof that the ‘kernel’ set theory whose postulates are extensionality. (E), and single-element adjunction and removal. (W) and (L), cannot be axiomatized by means of three-variable sentences. This highlights a sharp edge to be crossed in order to attain an ‘algebraization’ of Set Theory. Indeed, one easily shows that the theory which results from the said kernel by addition of the null set axiom, (N), is in its entirety expressible in three variables. Andrea Formisano 0001, Eugenio G. Omodeo, Alberto Policriti |
J. Symb. Log. | 1 |
| 2004 | Three-variable statements of set-pairing
Andrea Formisano 0001, Eugenio G. Omodeo, Alberto Policriti |
Theor. Comput. Sci. | 1 |
| 2003 | Compiling dyadic first-order specifications into map algebra
Domenico Cantone, Andrea Formisano 0001, Eugenio G. Omodeo, Calogero G. Zarba |
Theor. Comput. Sci. | 2 |
| 2000 | Goals and Benchmarks for Automated Map Reasoning
Andrea Formisano 0001, Eugenio G. Omodeo, Marco Temperini |
J. Symb. Comput. | 1 |
| 1999 | T-Resolution: Refinements and Model Elimination
Andrea Formisano 0001, Alberto Policriti |
J. Autom. Reason. | 1 |