In
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
, FO(.) (a.k.a. FO-dot) is a
knowledge representation
Knowledge representation (KR) aims to model information in a structured manner to formally represent it as knowledge in knowledge-based systems whereas knowledge representation and reasoning (KRR, KR&R, or KR²) also aims to understand, reason, and ...
language based on
first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
(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.
* Ty ...
, 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 , .
Models can be divided int ...
, answering set queries, checking
entailment
Logical consequence (also entailment or logical implication) 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 l ...
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 ...
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 from ''A'' to ''B'',
denotes
integer
An integer is the number zero (0), a positive natural number (1, 2, 3, ...), or the negation of a positive natural number (−1, −2, −3, ...). The negations or additive inverses of the positive natural numbers are referred to as negative in ...
s,
denotes the
booleans,
¬ denotes
negation
In logic, negation, also called the logical not or logical complement, is an operation (mathematics), operation that takes a Proposition (mathematics), proposition P to another proposition "not P", written \neg P, \mathord P, P^\prime or \over ...
, and
⇒ denotes
material conditional
The material conditional (also known as material implication) is a binary operation commonly used in logic. When the conditional symbol \to is interpreted as material implication, a formula P \to Q is true unless P is true and Q is false.
M ...
. Predicates < and ≥ are built-in and have their usual meaning.
Such knowledge base can be turned automatically into an Interactive Lawyer (see here
)
References
External links
*
{{Automated reasoning
Knowledge representation languages