Theorem proving for non-normal modal logics
Theorem proving for non-normal modal logics
In this work we briefly summarize our recent contributions in the field of proof methods, theorem proving and countermodel generation for non-normal modal logics. We first recall some labelled sequent calculi for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. Then, we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof in the labelled calculi, otherwise it is able to extract a model falsifying it from an open, saturated branch. © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
Peer reviewed
- University of Helsinki Finland
- AIX-Marseille Université France
- Aix-Marseille University France
- Aix Marseille Université (La Timone) France
- Aix-Marseille Université France
Biomineralization, Artificial intelligence, Theorem provers, Differentiation (calculus), Modal logic, Proof methods, Computer circuits, Formal logic, Sequent calculus, Semantics, Formal verification, Modal formulas, Philosophy, Basic systems, Pathology, Neighbourhood, Robots, Theorem proving, Automata theory
Biomineralization, Artificial intelligence, Theorem provers, Differentiation (calculus), Modal logic, Proof methods, Computer circuits, Formal logic, Sequent calculus, Semantics, Formal verification, Modal formulas, Philosophy, Basic systems, Pathology, Neighbourhood, Robots, Theorem proving, Automata theory
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!