Stack Overflow
Stack Overflow

Questions tagged [modal-logic]

Programming questions that essentially involve modal logic, the branch of logic concerning modalities such as possibility, belief, and tenses. For questions about modal dialogs, use [modal-dialog] instead.

14 questions
10
votes
1 answer

Interesting operators in Haskell that obey modal axioms

I was just looking at the type of map :: (a -> b) -> [a] -> [b] and just the shape of this function made me wonder whether we could see the list forming operator [ ] as obeying various axioms common to normal modal logics (e.g, T, S4, S5, B), since…
user65526
  • 685
  • 6
  • 19
9
votes
9 answers

P implies Q, how to read in english

how to read P implies Q in classical logic? example : Distributivity: Ka(X->Y) -> (KaX -> KaY) This is modal logic which uses classical logic rules. KaX : a knows the that X is true. I m curious about how to read implication in english? if…
DarthVader
  • 52,984
  • 76
  • 209
  • 300
7
votes
1 answer

Extending propositional logic to modal logic in Haskell

I have written some code in Haskell for modeling propositional logic data Formula = Prop {propName :: String} | Neg Formula | Conj Formula Formula | Disj Formula Formula | Impl Formula Formula …
Jetze
  • 73
  • 5
5
votes
1 answer

prolog catch all clause that's only active if no other clause is

I have a predicate that relates a modal logic formula to its negative normal form. All connectives except the modal operators, conjunction, and disjunction are eliminated, and negation is pushed as far into the leaves of the expression as…
Greg Nisbet
  • 6,710
  • 3
  • 25
  • 65
4
votes
2 answers

Kripke semantics: learning software available?

I am stuck on Kripke semantics, and wonder if there is educational software through which I can test equivalence of statements etc, since Im starting to think its easier to learn by example (even if on abstract variables). I will use ☐A to write…
propaganda
  • 470
  • 2
  • 6
  • 14
4
votes
2 answers

python modal logic K solver

I am working on modal logic tableau solver which is implemented in python (2.7.5 version). So I already have a function that translates an input string to tableau format that is: Input： ~p ^ q Parsed: ['and',('not', 'p'), 'q'] Parsed and alpha…
marcincuber
  • 3,451
  • 1
  • 17
  • 29
4
votes
2 answers

Solvers for modal epistemic logics

Is there any (SMT-like) solvers for modal epistemic logics (aka logic of knowledge)? I need First Order (not just propositional) case.
mart
  • 2,537
  • 1
  • 15
  • 13
2
votes
1 answer

(New?) Modal Operators for Foldable

This post follows in a sense my previous one. HTNW, in their answer there, defined the data type Same and the function allEq. So I thought that by defining the data type AllDifferent, the function allDiff and the derived ones someEq and someDiff, I…
Alberto Capitani
  • 1,039
  • 13
  • 30
2
votes
2 answers

Change the parsing language

I'm using a modal-SAT solver. This solver is unfortunately using Flex and Bison, both languages that I don't master... I wanted to change one syntax to another, but I've got some issue to do it, even after tutorials about Flex-Lexer and Bison. So…
Valentin Montmirail
  • 2,594
  • 1
  • 25
  • 53
1
vote
1 answer

NuSMV returns undefined operation

I have written the following code: MODULE main VAR status:{empty, no_empty}; x : 0..3; ASSIGN init(status):= empty; init(x):=0; next(status):= case (status = empty): no_empty; (status = no_empty) & (x=0):…
Gold
  • 179
  • 2
  • 11
1
vote
1 answer

Can modal operator be defined as a boolean function?

Let us consider for simplicity only Kripke structures with a single agent whose knowledge is described by the modal operator K. We know that in all the corresponding Kripke structures where K is interpreted by equivalence there holds for any…
David
  • 112
  • 1
  • 8
0
votes
0 answers

Kripke structure, modal logic

I would appreciate help with how to interpret a Kripke model. I want to determine in which of the world, , of s_1-s_6, the negation to p exists ($\neg p$) but do not know how to think about an empty world or one that contains both p and q, which in…
user15415514
  • 31
  • 5
0
votes
0 answers

Logical operations in modal three-valued logic (XOR, IMP EQV)

From my understanding, the modal quantifier possibly relaxes the behaviour of logical conjunction: (true) and (possibly false) => true (true) and (possibly unknown) => true (possibly true) and (possibly false) …
AlexDarkVoid
  • 485
  • 3
  • 12
0
votes
1 answer

inconsistent formulaes in the list python

So the question relates to List of lists that store different propositional modal formulaes. I am capable of removing duplicates but I don't know how to find inconsistances. So for example: Initial List of lists: [[('not', ('box', 'p')), ('box',…
marcincuber
  • 3,451
  • 1
  • 17
  • 29