In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, FO(.) (a.k.a. FO-dot) is a
knowledge representation
Knowledge representation and reasoning (KRR, KR&R, KR²) is the field of artificial intelligence (AI) dedicated to representing information about the world in a form that a computer system can use to solve complex tasks such as diagnosing a medic ...
language based on
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
(FO). It extends FO with
types
Type may refer to:
Science and technology Computing
* Typing, producing text via a keyboard, typewriter, etc.
* Data type, collection of values used for computations.
* File type
* TYPE (DOS command), a command to display contents of a file.
* Typ ...
, 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
A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure.
Models c ...
, answering set queries, checking
entailment
Logical consequence (also entailment) is a fundamental concept in logic, which describes the relationship between statements that hold true when one statement logically ''follows from'' one or more statements. A valid logical argument is one ...
between two theories and checking
satisfiability
In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...
, among other types of inference over a FO(.) knowledge base.
FO(.) has four types of statements:
* Type, function and predicate declarations,
*
Axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s, 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
theory T:V
In this code, ''A''
→''B'' indicates a
function
Function or functionality may refer to:
Computing
* Function key, a type of key on computer keyboards
* Function model, a structured representation of processes in a system
* Function object or functor or functionoid, a concept of object-oriente ...
from ''A'' to ''B'',
denotes
integer
An integer is the number zero (), a positive natural number (, , , etc.) or a negative integer with a minus sign (−1, −2, −3, etc.). The negative numbers are the additive inverses of the corresponding positive numbers. In the language ...
s,
denotes the
booleans,
¬ denotes
negation
In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P, \mathord P or \overline. It is interpreted intuitively as being true when P is false, and false ...
, and
⇒ denotes
material conditional
The material conditional (also known as material implication) is an operation commonly used in logic. When the conditional symbol \rightarrow is interpreted as material implication, a formula P \rightarrow Q is true unless P is true and Q is ...
. Predicates < and ≥ are built-in and have their usual meaning.
Such knowledge base can be turned automatically into an Interactive Lawyer (see here
)
References
{{reflist
External links
The FO(.) language
Knowledge representation languages