What are the future prospects in near future from a theoretical investigation of description logics, and modal logics in the context of artificial intelligence research?
Asked
Active
Viewed 148 times
1 Answers
0
Temporal logic is a highly practical subset of modal logic, and is often exploited for formal methods and formal verification (especially model checking).
E.g., it is used to model temporal behavior of digital circuits (synchronous/asynchronous) and embedded systems via formal methods, and exploited via model checking (to reduce effort in people-hours spend on verification, testing, and validation). Cyber-physical systems are harder to verify, since they involve hybrid systems and tend to favor satisfiability modulo theories (SMT). This is because SMT is decidable, while its first-order logic superset is undecidable in general.
I note that there is an overlap between description logics and modal logics, so you can explore a better scope/definition for this subset. Or, simply just focus on hot topics involving practical applications of temporal logic for formal verification.
In theory, theorem provers for formal verification can process formulas for the entire set of first-order logic, which is undecidable as aforementioned.
However, SMT solvers can solve decidable decision problems involving fragments of first-order logic and their combinations. SMT solvers are based on solvers for the boolean/propositional satisfiability (SAT) problem, or SAT solvers. As the GRASP and Chaff SAT solvers drove researchers to achieve an exponential improvement in performance of SAT solvers by 7 orders of magnitude, from the late 1990s till 2011 (or the early 2010s), SMT solvers leverage this growing performance speedup to improve their performance and capabilities. Hence, SAT solvers, followed by SMT solvers, are used to improve the performance and capabilities of model checking software in this time period.
Specifically, hybrid theorem proving systems involve model checking and theorem proving. Hence, this is still a viable topic for exploration, especially for cyber-physical systems and networks thereof. This is important, since networked cyber-physical systems include Internet of Things (IoT) systems/networks and support distributed/federated machine learning.
Hence, there are aspects of modal logic that are relevant for theoretical AI (or AI theory, if you like) and applied AI (e.g., formal verification).
As for good old knowledge representation, avoid expert systems at all costs. Yes, their main problem is the computational complexity in automated (logical) reasoning of logical formulas. Decision procedures (for SAT/SMT solvers) are a subset of automated reasoning, a popular and important subset of logical AI, thanks to the aforementioned SAT/SMT solver improvement. However, the exponential performance speedup/improvement of SAT/SMT solvers cannot keep up with the potential exponential increase of logic formulas that expert systems need. This is because expert systems need to keep up to date with the increasing complexity of modern/contemporary engineering systems.
In terms of information mapping, semantic networks are old, and the Semantic Web research activities have faded... Thanks to the ongoing boom in statistical/probabilistic machine learning, especially deep learning, which people are pivoting to or making use of.
That said, you can certainly combine techniques for statistical/probabilistic machine learning with SAT/SMT solver research, formal verification, and/or knowledge representation.
Giovanni
- 1
- 2