HiLog

Last updated

HiLog is a programming logic with higher-order syntax, which allows arbitrary terms to appear in predicate and function positions. [1] However, the model theory of HiLog is first-order. Although syntactically HiLog strictly extends first order logic, HiLog can be embedded into this logic.

Contents

HiLog was first described in 1989. [2] It was later extended in the direction of many-sorted logic. [3]

The XSB system parses HiLog syntax, but the integration of HiLog into XSB is only partial. In particular, HiLog is not integrated with the XSB module system. A full implementation of HiLog is available in the Flora-2 system.

It has been shown that HiLog can be embedded into first-order logic through a fairly simple transformation. [1] For instance, p(X)(Y,Z(V)(W)) gets embedded as the following first-order term: apply(p(X),Y,apply(apply(Z,V),W)). [1]

The Framework for Logic-Based Dialects (RIF-FLD) of the Rule Interchange Format (RIF) is largely based on the ideas underlying HiLog and F-logic. [4]

Examples

In all the examples below, capitalized symbols denote variables and the comma denotes logical conjunction, as in most logic programming languages. The first and the second examples show that variables can appear in predicate positions. Predicates can even be complex terms, such as closure(P) or maplist(F) below. The third example shows that variables can also appear in place of atomic formulas, while the fourth example illustrates the use of variables in place of function symbols. The first example defines a generic transitive closure operator, which can be applied to an arbitrary binary predicate. The second example is similar. It defines a LISP-like mapping operator, which applies to an arbitrary binary predicate. The third example shows that the Prolog meta-predicate call/1 can be expressed in HiLog in a natural way and without the use of extra-logical features. The last example defines a predicate that traverses arbitrary binary trees represented as first-order terms.

closure(P)(X,Y)<-P(X,Y).closure(P)(X,Y)<-P(X,Z),closure(P)(Z,Y).maplist(F)([],[]).maplist(F)([X|R],[Y|Z])<-F(X,Y),maplist(F)(R,Z).call(X)<-X.traverse(X(L,R))<-traverse(L),traverse(R).

Related Research Articles

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 quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

Prolog is a logic programming language associated with artificial intelligence and computational linguistics.

Arity is the number of arguments or operands taken by a function, operation or relation in logic, mathematics, and computer science. In mathematics, arity may also be named rank, but this word can have many other meanings in mathematics. In logic and philosophy, it is also called adicity and degree. In linguistics, it is usually named valency.

In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other words, it is the predication of a property or relation to every member of the domain. It asserts that a predicate within the scope of a universal quantifier is true of every value of a predicate variable.

Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.

Datalog is a declarative logic programming language. While it is syntactically a subset of Prolog, Datalog generally uses a bottom-up rather than top-down evaluation model. This difference yields significantly different behavior and properties from Prolog. It is often used as a query language for deductive databases. In recent years, Datalog has found new application in data integration, information extraction, networking, program analysis, security, cloud computing and machine learning.

In computer science, the occurs check is a part of algorithms for syntactic unification. It causes unification of a variable V and a structure S to fail if S contains V.

Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

In logic, the formal languages used to create expressions consist of symbols, which can be broadly divided into constants and variables. The constants of a language can further be divided into logical symbols and non-logical symbols.

In logic, the monadic predicate calculus is the fragment of first-order logic in which all relation symbols in the signature are monadic, and there are no function symbols. All atomic formulas are thus of the form , where is a relation symbol and is a variable.

Abductive logic programming (ALP) is a high-level knowledge-representation framework that can be used to solve problems declaratively based on abductive reasoning. It extends normal logic programming by allowing some predicates to be incompletely defined, declared as abducible predicates. Problem solving is effected by deriving hypotheses on these abducible predicates as solutions of problems to be solved. These problems can be either observations that need to be explained or goals to be achieved. It can be used to solve problems in diagnosis, planning, natural language and machine learning. It has also been used to interpret negation as failure as a form of abductive reasoning.

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics.

The syntax and semantics of Prolog, a programming language, are the sets of rules that define how a Prolog program is written and how it is interpreted, respectively. The rules are laid out in ISO standard ISO/IEC 13211 although there are differences in the Prolog implementations.

In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact.

Flora-2 is an open source semantic rule-based system for knowledge representation and reasoning. The language of the system is derived from F-logic, HiLog, and Transaction logic. Being based on F-logic and HiLog implies that object-oriented syntax and higher-order representation are the major features of the system. Flora-2 also supports a form of defeasible reasoning called Logic Programming with Defaults and Argumentation Theories (LPDA). Applications include intelligent agents, Semantic Web, knowledge-bases networking, ontology management, integration of information, security policy analysis, automated database normalization, and more.

In logic, a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula. For instance, the universal quantifier in the first order formula expresses that everything in the domain satisfies the property denoted by . On the other hand, the existential quantifier in the formula expresses that there exists something in the domain which satisfies that property. A formula where a quantifier takes widest scope is called a quantified formula. A quantified formula must contain a bound variable and a subformula specifying a property of the referent of that variable.

In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query languages, in particular to Datalog.

<span class="mw-page-title-main">Semantic Web Services Language</span>

The Semantic Web Services Language (SWSL) is a general-purpose logical language for specifying Semantic Web Services Ontologies (SWSOs), as well as individual Web services. The Semantic Web Services Language (SWSL) describes the syntax elements of SWSL and its semantic and semantic foundations. It can be used with the underlying language and network structure of Semantic Web Services. Syntactically, first-order logic is a subset of the Semantic Web Services Language (SWSL).

Flix is a functional, imperative, and logic programming language developed at Aarhus University, with funding from the Independent Research Fund Denmark, and by a community of open source contributors. The Flix language supports algebraic data types, pattern matching, parametric polymorphism, currying, higher-order functions, extensible records, channel and process-based concurrency, and tail call elimination. Two notable features of Flix are its type and effect system and its support for first-class Datalog constraints.

References

  1. 1 2 3 Chen, Weidong; Kifer, Michael; Warren, David S. (February 1993). "HiLog: A foundation for higher-order logic programming". Journal of Logic Programming . 15 (3): 187–230. doi: 10.1016/0743-1066(93)90039-J .
  2. ↑ Chen, Weidong; Kifer, Michael; Warren, David S. (1989). "HiLog: a first order semantics for higher-order logic programming constructs". Logic programming: Proceedings of the North American conference, 1989. MIT Press. ISBN   0262620642. OCLC   1153667751.
  3. ↑ Chen, Weidong; Kifer, Michael (1995). "Sorted HiLog: sorts in higher-order logic data languages". In Gottlob, Georg; Vardi, Moshe Y. (eds.). Database theory—ICDT '95: 5th International Conference, Prague, Czech Republic, January 11–13, 1995: proceedings. Lecture notes in computer science. Vol. 893. Springer. pp. 252–265. doi:10.1007/3-540-58907-4_20. ISBN   9780387589077. OCLC   31740400.
  4. ↑ Kifer, Michael (2008). "Rule interchange format: the framework". In Calvanese, Diego; Lausen, Georg (eds.). Web reasoning and rule systems: second international conference, RR 2008, Karlsruhe, Germany, October 31–November 1, 2008: proceedings. Lecture notes in computer science. Vol. 5341. Springer. pp. 1–11. doi:10.1007/978-3-540-88737-9_1. ISBN   9783540887362. OCLC   262884460.

Further reading

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.