Cited By
View all- Ehlers RLange M(2014)A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal LogicAutomated Reasoning10.1007/978-3-319-08587-6_27(360-366)Online publication date: 2014
Finite satisfiability of propositional interval logic formulas with multi-objective evolutionary algorithms
Pages 25 - 36
Abstract
Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. Despite being relevant for a broad spectrum of application domains, ranging from temporal databases to artificial intelligence and verification of reactive systems, interval temporal logics still misses algorithms and tools capable of supporting them in an efficient way. In this paper, we approach the finite satisfiability problem for the simplest meaningful interval temporal logic (which is NEXPTIME-complete), namely A (also known as Right Propositional Neighborhood Logic), by means of a multi-objective combinatorial optimization model solved with three different multi-objective evolutionary algorithms. As a result we obtain a decision procedure that, although incomplete, turns out to be unexpectedly suitable and easy to implement with respect to classical complete algorithms. Moreover, this approach allows one to effectively search for the minimal model that satisfy a set of A-formulas without using any kind of normal form.
References
[1]
L. Aksoy and E. Gunes. An evolutionary local search algorithm for the satisfiability problem. In Proc. of the 14th Turkish conference on Artificial Intelligence and Neural Networks, pages 185--193. Springer, 2006.
[2]
J. F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832--843, 1983.
[3]
D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification. In Proc. of 15th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, volume 5330 of LNCS, pages 590--604. Springer, 2008.
[4]
D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Metric propositional neighborhood logic: Expressiveness, decidability, and undecidability. In Proc. of the 19th European Conference on Artificial Intelligence (ECAI), pages 695--700. IOS Press, 2010.
[5]
D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Metric propositional neighborhood logics on natural numbers. Software and Systems Modeling, pages 1--20, 2011. 10.1007/s10270-011-0195-y.
[6]
D. Bresolin, V. Goranko, A. Montanari, and G. Sciavicco. Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions. Annals of Pure and Applied Logic, 161(3):289--304, 2009.
[7]
D. Bresolin, A. Montanari, and G. Sciavicco. An optimal decision procedure for Right Propositional Neighborhood Logic. Journal of Automated Reasoning, 38(1-3):173--199, 2007.
[8]
D. Bresolin, P. Sala, and G. Sciavicco. On begins, meets, and before. International Journal on Foundations of Computer Science, 3(23):559--583, 2012.
[9]
C. C. Coello, D. V. Veldhuizen, and G. Lamont. Evolutionary Algorithms for Solving Multi-Objective Problems (Genetic Algorithms and Evolutionary Computation). Springer, 2002.
[10]
K. Deb. Multi-Objective Optimization Using Evolutionary Algorithms. Wiley, 2001.
[11]
H. Ellerweg. A Study of Evolutionary Algorithms for the Satisfiability Problem. PhD thesis, University of Paderborn, 2004.
[12]
E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 995--1072. MIT Press, 1990.
[13]
E. Giunchiglia, A. Tacchella, and F. Giunchiglia. Sat-based decision procedures for classical modal logics. Journal of Automed Reasoning, 28(2):143--171, 2002.
[14]
A. Gómez-Skarmeta, F. Jiménez, and G. Sánchez. Improving interpretability in approximative fuzzy models via multiobjective evolutionary algorithms. International Journal of Intelligent Systems, 22(9):943--969, 2007.
[15]
V. Goranko, A. Montanari, and G. Sciavicco. A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics, 14(1--2):9--54, 2004.
[16]
J. Gottlieb, E. Marchiori, and C. Rossi. Evolutionary algorithms for the satisfiability problem. Evolutionary Computation, 10(1):35--50, 2002.
[17]
J. Halpern and Y. Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38(4):935--962, 1991.
[18]
I. Horrocks. Using an expressive description logic: Fact or fiction? In Proc. of the 6th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 636--649, 1998.
[19]
U. Hustadt and R. Schmidt. An empirical analysis of modal theorem provers. Journal of Applied Non-Classical Logics, 9(4):479--522, 1999.
[20]
F. Jiménez, G. Sánchez, J. Cadenas, A. Gómez-Skarmeta, and J. Verdegay. Nonlinear optimization with fuzzy constraints by multi-objective evolutionary algorithms. In Proc. of the 8th Computational Intelligence, Theory and Applications International Conference Fuzzy Days, pages 713--722. Springer, 2004.
[21]
H. Jin-Kao, F. Lardeux, and F. Saubion. Evolutionary computing for the satisfiability problem. In Proc. of the 3rd European Workshop on Evolutionary Computation in Combinatorial Optimization, volume 2611 of LNCS, pages 258--268. Springer, 2003.
[22]
J. Koza, editor. Solving Satisfiability Problems with Genetic Algorithms, pages 206--213. Stanford Bookstore, 2000.
[23]
D. D. Monica, D. Bresolin, A. Montanari, and G. Sciavicco. Interval temporal logics over finite linear orders:the complete picture. In Proc. of the 20th European Conference on Artificial Intelligence (in publication), 2012.
[24]
A. Montanari, G. Puppis, and P. Sala. Maximal decidable fragments of Halpern and Shoham's modal logic of intervals. In ICALP (2), pages 345--356, 2010.
[25]
M. O'Mahony. Sensory Evaluation of Food: Statistical Methods and Procedures. CRC Press, 1986.
[26]
P. Patel-Schneider. Dlp system description. In Proc. of the 11th Description Logics Workshop (DL), pages 87--89, 1998.
[27]
P. Patel-Schneider and R. Sebastiani. A new general method to generate random modal formulae for testing decision procedures. Journal of Artificial Intelligence Research, 18:351--389, 2003.
[28]
C. Rossi, E. Marchiori, and J. Kok. An adaptive evolutionary algorithm for the satisfiability problem. In Proc. of the ACM symposium on Applied computing, volume 1, pages 463--469. ACM, 2000.
[29]
M. Srinivas and P. L.M. Adaptive probabilities of crossover and mutation in genetic algorithms. IEEE Transactions on Systems, Man and Cybernetics, 4(24):656--667, 1994.
[30]
M. Stol and M. D. Rijke. Modal logic and local search. In Proc. of the KI-2001 Workshop on Modal Logic and Artificial Intelligence, 2001.
Index Terms
- Finite satisfiability of propositional interval logic formulas with multi-objective evolutionary algorithms
Recommendations
Deciding Regular Grammar Logics with Converse Through First-Order Logic
We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF 2 , which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically ...
The 0-1 law fails for frame satisfiability of propositional modal logic
LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer ScienceThe digraph property KERNEL is a very simple and well-known property studied in various areas. We previously defined a variant of this property as a counterexample of 0-1law for the monadic existential second order logic with at most two first-order ...
Reducts of propositional theories, satisfiability relations, and generalizations of semantics of logic programs
Over the years, the stable-model semantics has gained a position of the correct (two-valued) interpretation of default negation in programs. However, for programs with aggregates (constraints), the stable-model semantics, in its broadly accepted ...
Comments
Information & Contributors
Information
Published In
January 2013
198 pages
Copyright © 2013 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 16 January 2013
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
FOGA '13
Sponsor:
Acceptance Rates
Overall Acceptance Rate 72 of 131 submissions, 55%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 70Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 03 Mar 2025
Other Metrics
Citations
Cited By
View all- Ehlers RLange M(2014)A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal LogicAutomated Reasoning10.1007/978-3-319-08587-6_27(360-366)Online publication date: 2014
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in