10
votes
Accepted
Framework or tools to generate theorem prover/solver/reasoner for new logic
There are many related ways you can mechanise your logic.
Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using ...
- 8,358
10
votes
Accepted
Why is this expression (A and ¬A |= C) entailed?
The statement $X\vDash Y$ means "every assignment to the variables that makes $X$ true also makes $Y$ true." Or to put it another way, "There is no assignment of variables that makes $X$ true but ...
- 82.1k
7
votes
Do we have knowledge bases only because the logics are not automated enough?
Most logical systems in use are automated enough in principle. That is, there are algorithms which find the proof of a statement, if such a proof exists. The problem is computational complexity. Such ...
- 31k
3
votes
Trying to understand interpretation and denotation in FOL
Consider the expression $+(x,\times(y,y))$, which is the FOL way to write $x+(y\cdot y)$. If I substitute $x=3$ and $y=5$ and do the arithmetic over the integers, what do I get? I need to evaluate the ...
- 278k
2
votes
Accepted
Why there is forward chaining inference engine (reasoner) for description logics only and not for other logics?
This question is a bit strange. I see it's based on the Wikipedia article, but that article is also a bit strange. I will try to clarify some concepts.
First, we have a language that can be used to ...
- 727
1
vote
List of all possible reasoning tasks - satisfiability and theorem proving only?
There is no exhaustive list of reasoning tasks, as the phrase "reasoning task" does not have a precise definition.
Don't put too much weight on categorizations. They're a descriptive tool that might ...
D.W.♦
- 164k
1
vote
Proving whether $\bf{K}$(Happy $\lor$Sad) $\implies$ $\neg \bf{K}($Happy) is satisfiable, valid or unsatisfiable
The formula is either satisfiable or unsatisfiable. Only when it is satisfiable, it may also be valid.
To rule out that the implication is valid, show that its negation is satisfiable, that is, ...
- 917
Only top scored, non community-wiki answers of a minimum length are eligible