Misplaced Pages

FO(.)

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Knowledge representation computer programming language
This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages)
This article's use of external links may not follow Misplaced Pages's policies or guidelines. Please improve this article by removing excessive or inappropriate external links, and converting useful links where appropriate into footnote references. (January 2022) (Learn how and when to remove this message)
A major contributor to this article appears to have a close connection with its subject. It may require cleanup to comply with Misplaced Pages's content policies, particularly neutral point of view. Please discuss further on the talk page. (February 2022) (Learn how and when to remove this message)
The topic of this article may not meet Misplaced Pages's general notability guideline. Please help to demonstrate the notability of the topic by citing reliable secondary sources that are independent of the topic and provide significant coverage of it beyond a mere trivial mention. If notability cannot be shown, the article is likely to be merged, redirected, or deleted.
Find sources: "FO(.)" – news · newspapers · books · scholar · JSTOR (February 2022) (Learn how and when to remove this message)
(Learn how and when to remove this message)

In computer science, FO(.) (a.k.a. FO-dot) is a knowledge representation language based on first-order logic (FO). It extends FO with types, aggregates (counting, summing, maximising ... over a set), arithmetic, inductive definitions, partial functions, and intensional objects.

By itself, a FO(.) knowledge base cannot be run, as it is just a "bag of information", to be used as input to various generic reasoning algorithms. Reasoning engines that use FO(.) include IDP-Z3, IDP and FOLASP. As an example, the IDP system allows generating models, answering set queries, checking entailment between two theories and checking satisfiability, among other types of inference over a FO(.) knowledge base.

FO(.) has four types of statements:

  • Type, 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.

Example

A voting law specifies that citizens must be at least 18 years old to vote. Furthermore, if the voting law is interpreted as being prescriptive, voting is mandatory when you are over 18. This can be 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, AB indicates a function from A to B, Z {\displaystyle \mathbb {Z} } denotes integers, B {\displaystyle \mathbb {B} } denotes the booleans, ¬ denotes negation, and denotes material conditional. Predicates < and ≥ are built-in and have their usual meaning.

Such knowledge base can be turned automatically into an Interactive Lawyer (see here)

References

  1. Denecker, Marc (2000). "Extending classical logic with inductive definitions". International Conference on Computational Logic: 703–717. arXiv:cs/0003019. Bibcode:2000cs........3019D.
  2. "IDP-Z3". Retrieved 2022-02-01.
  3. 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. pp. 279–323. doi:10.1145/3191315.3191321. ISBN 9781970001990. S2CID 3866665.
  4. "IDP". Retrieved 2022-02-01.
  5. "FOLASP". Retrieved 2022-02-01.
  6. "Interactive Consultant". Retrieved 2022-02-01.
  7. "Interactive Lawyer". Retrieved 2022-02-01.

External links

Knowledge representation and reasoning
Expert systems
Reasoning systems
Ontology languages
Theorem provers
Constraint satisfaction
Automated planning
Category: