# Tag Info

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
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

### 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

### 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
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 ...
• 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