FO(.): Difference between revisions
→top: keep lead-sentence source; rm redundant url (same page as doi) |
FO(.) paper |
||
| Line 1: | Line 1: | ||
{{external links|date=January 2022}} |
{{external links|date=January 2022}} |
||
In [[computer science]], '''FO(.)''' (a.k.a. '''FO-dot''') is a [[Knowledge representation and reasoning|knowledge representation]] language based on [[first-order logic]].<ref |
In [[computer science]], '''FO(.)''' (a.k.a. '''FO-dot''') is a [[Knowledge representation and reasoning|knowledge representation]] language based on [[first-order logic]].<ref>{{cite journal |last1=Denecker |first1=Marc |title=Extending classical logic with inductive definitions |journal=International Conference on Computational Logic |date=2000 |pages=703-717 |doi= |url=https://arxiv.org/pdf/cs/0003019}}</ref> |
||
It has 4 types of statements: |
It has 4 types of statements: |
||
* Function and predicate declarations, |
* Function and predicate declarations, |
||
Revision as of 09:17, 1 February 2022
 | This article's use of external links may not follow Wikipedia's policies or guidelines. (January 2022) |
In computer science, FO(.) (a.k.a. FO-dot) is a knowledge representation language based on first-order logic.[1]
It has 4 types of statements:
- Function and predicate declarations,
- Axioms, i.e., logic sentences about possible worlds,
- Definitions that specify a unique interpretation of a defined symbol, given the interpretation of its parameters. Definitions can be inductive.
- Enumerations, i.e., definitions of symbols by enumeration.
An FO-dot knowledge base cannot be run. It is a "bag of information", to be used as input to various generic reasoning algorithms: e.g., to determine relevant questions, to compute consequences of new facts, and to explain them.
FO(.) extends first-Order logic with: types, aggregates, arithmetic, (inductive) definitions, partial functions, and intensional objects.
FO-dot is used by these reasoning engines:
- IDP-Z3[2]
- FOLASP[5]
Example
The following voting laws
- you must be at least 18 years old to vote;
- if the law is prescriptive, voting is mandatory.
can represented in FO(.) as follows:
vocabulary V{
age: () → ℤ // function declaration
prescriptive, vote: () → 𝔹 // predicate declarations
}
theory T:V {
age()< 18 ⇒ ¬vote(). // axiom: if you are less than 18, you may not vote.
prescriptive() ⇒ (age()≥ 18 ⇒ vote()). // axiom: if prescriptive: if you are at least 18, you must vote
}In this code, A→B indicates a function from A to B; 𝔹 denotes the booleans, ¬ denotes negation, and ⇒ denotes material conditional.
Such knowledge base can be turned automatically into an Interactive Lawyer[6] (see here[7]
References
- ^ Denecker, Marc (2000). "Extending classical logic with inductive definitions". International Conference on Computational Logic: 703–717.
- ^ "IDP-Z3". Retrieved 2022-02-01.
- ^ De Cat, Broes; Bogaerts, Bart; Bruynooghe, Maurice; Janssens, Gerda; Denecker, Marc (2018). "Predicate logic as a modeling language: the IDP system". Declarative Logic Programming: Theory, Systems, and Applications: 279–323. doi:10.1145/3191315.3191321.
- ^ "IDP". Retrieved 2022-02-01.
- ^ "FOLASP". Retrieved 2022-02-01.
- ^ "Interactive Consultant". Retrieved 2022-02-01.
- ^ "Interactive Consultant". Retrieved 2022-02-01.