We changed our privacy policy. Read more.
11

I will just write what Frank Pfenning taught me (all mistakes go on my account). A traditional formal system in logic, such as natural deduction, is descriptive in the sense that it tells us what valid deductions are, but it does not tell us how we are supposed to look for them. The starting point of logic programming is to take the rules of deduction and ...


8

FO-LFP is neither complete (its valid sentences cannot be described by a recursively presented proof system) nor compact (there is an unsatisfiable set of sentences all of whose finite subsets are satisfiable). The basic argument is given in Denis’s answer so I won’t repeat it here, but let me instead point out that as a general principle due to Per ...


6

You should have a look at Uniform Proofs as a Foudation for Logic Programming by Dale Miller, Gopalan Nadathur, Frank Pfenning and Andre Scedrov, 1991. The idea of this work and the rich area that has seen spawn from these ideas is to understand the execution of a logic program as proof search in simple and expressive logics, such as intuitionistic logic or ...


6

Any logic defined semantically in a similar way is trivially consistent, as it has a model. Any finite-valued logic has a faithful translation into classical logic, hence its set of valid formulas, or even the consequence relation, are recursively enumerable. Completeness is a relationship between semantics and a proof system. You only gave the semantics, ...


5

Let's assume that your three-valued logic consists of the truth values Yes, No and "unknown". We can think of these truth values as the sets $\{\top\}, \{\bot\}, \{\top,\bot\}$, and then the logical operations result in all possible values. For example, Yes and Unknown is Unknown while No and Unknown is No. A trick known as "double rail logic" uses two ...


4

Prolog embodies the idea of computation as proof search. That is: a program is a formula which we would like to satisfy, the computation is the proof search, and the result is the witness for the formula. To make this idea work we need to reformulate the rules of first-order logic so that they can be read as instructions for execution of a proof search. We ...


4

What do you mean by the equality in your first formula? In first-order logic (FOL) with equality, one can only apply the equality operator to a couple of terms, not to formulae. Also, your use of equality cannot be considered a case of definition (what could be better depicted by $\triangleq$) since the predicate List appears on both sides of the equality. ...


2

It does not extend. Consider FO-LFP with just a binary predicate $<$, and the axioms for $<$ being a total order, with first and last positions, and every position has a successor. Moreover, we add an axiom saying that the last position can be reached from the first by iterating the successor function as a smallest fixpoint. This ensures that the ...


2

Your translation goes into Presburger arithmetic, which is decidable. You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. Since pretty much all SMT solvers are (fancy extensions of) DPLL, I would guess you can turn those proofs into resolution proofs without too much difficulty. ...


1

I have concluded that one cannot add both + and × in the λProlog programming language with their arithmetic semantics since the decision problem is undeciable. Because if it was decidable then Hilbert's tenth problem would have a positive answer. See the Wikipedia page for Hilbert's tenth problem.


1

If your setting is FOL then why not just use a FOL theorem prover. What is unclear from your question is what you mean by general case. Using a FOL theorem prover covers any such query you could write in FOL... although of course, FOL is semi-decidable so it is not guaranteed that you can get an answer. Your problem can be written in the TPTP language as ...


1

What semantics of the logical operators would you like to have? Two of the best studied semantics for degrees are (propositional) Łukasiewicz logic and Gödel-Dummet logic. The latter enforces the domain to be a linear order which would allow you to model them via the naturals. It is also axiomatizable, since it is equivalent to intuitionistic propositional ...


1

Prolog deals with a formal system which is a small fragment of first order logic: it uses a logic of definite clauses, which are disjunctions of atoms and negated atoms, with the resolution rule as only inference rule. If you're not completely familiar to formal (logic) systems you just need to know that they are basically sets of rules: rules that ...


1

Not open source, but the AI engines of some successful computer games are based on modal logic, see e.g. "Using Exclusion Logic to Model Social Practices" and "Introducing Exclusion Logic as a Deontic Logic" by Richard Evans.


Only top voted, non community-wiki answers of a minimum length are eligible