China
Africa
Explore chapters and articles related to this topic
The Logic of Propositions and Predicates
Published in Konar Amit, Artificial Intelligence and Soft Computing, 2018
A logic is called decidable if there exists a method by which we can correctly say whether a given formula is valid or invalid. Readers may remember that validity of a formula α means satisfiability of the formula for all possible interpretations. A sound and complete proof method is able to prove the validity of a formula [3]. But if the formula is invalid, the proof procedure (by resolution principle or otherwise) will never terminate. This is called semi-decidablity. FOL is semi-decidable, as it is unable to prove the invalidity of a formula.
Copy and remove as dynamic operators
Published in Journal of Applied Non-Classical Logics, 2021
Carlos Areces, Hans van Ditmarsch, Raul Fervari, Bastien Maubert, François Schwarzentruber
In Areces et al. (2018a), Areces et al. (2012), Areces et al. (2014), and Fervari (2014), a family of logics called relation-changing logics are studied. These articles consider modalities with the ability of modifying the accessibility relation of a model while evaluating a formula. Three kinds of updates are considered, performing both local and global effects: adding, deleting and swapping around edges. All the obtained logics are very expressive (and all different), and they are computationally untractable (their satisfiability problem is undecidable). Among these modalities, the sabotage operator is particularly interesting, and it was also investigated in van Benthem (2005), Gierasimczuk et al. (2009), Löding and Rohde (2003), Löding and Rohde (2003). In one of its versions, sabotage deletes an arbitrary arrow in the model, and afterwards, formulas are evaluated in the updated model. In this sense, it is similar to the edge-removal modality studied in this paper. But while sabotage deletes edges arbitrarily in the model, the effects of depend on the satisfiability of certain formulas that are explicit in the operation. Thus, performs more uniform updates, leading to a decidable logic as we show in this article.