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
- Aix Marseille Université (La Timone) France
- Aix-Marseille Universite France
- Aix-Marseille Université France
- Aix-Marseille université France
- Aix-Marseille University France
Biomineralization, Artificial intelligence, Theorem provers, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], 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, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], 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
selected citations These citations are derived from selected sources.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!