Misplaced Pages

#174825

27-511: HiLog was first described in 1989. It was later extended in the direction of many-sorted logic . 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

54-424: A n i m a l {\displaystyle \mathrm {animal} } . While a function m o t h e r : a n i m a l → a n i m a l {\displaystyle \mathrm {mother} \colon \mathrm {animal} \to \mathrm {animal} } makes sense, a similar function m o t h e r : p l

81-471: A n t → p l a n t {\displaystyle \mathrm {mother} \colon \mathrm {plant} \to \mathrm {plant} } usually does not. Many-sorted logic allows one to have terms like m o t h e r ( l a s s i e ) {\displaystyle \mathrm {mother} (\mathrm {lassie} )} , but to discard terms like m o t h e r ( m y _ f

108-590: A v o r i t e _ o a k ) {\displaystyle \mathrm {mother} (\mathrm {my\_favorite\_oak} )} as syntactically ill-formed. The algebraization of many-sorted logic is explained in an article by Caleiro and Gonçalves, which generalizes abstract algebraic logic to the many-sorted case, but can also be used as introductory material. While many-sorted logic requires two distinct sorts to have disjoint universe sets, order-sorted logic allows one sort s 1 {\displaystyle s_{1}} to be declared

135-549: A fairly simple transformation. 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)) . 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 . In all the examples below, capitalized symbols denote variables and the comma denotes logical conjunction , as in most logic programming languages. The first and

162-446: A much wider variety of propositional logics. (3) owes much to the joint work of Blok and Pigozzi exploring the different forms that the well-known deduction theorem of classical propositional calculus and first-order logic takes on in a wide variety of logical systems. They related these various forms of the deduction theorem to the properties of the algebraic counterparts of these logical systems. Abstract algebraic logic has become

189-575: A programming example, a parametric sort list ( X ) {\displaystyle {\text{list}}(X)} may be declared (with X {\displaystyle X} being a type parameter as in a C++ template ), and from a subsort declaration int ⊆ float {\displaystyle {\text{int}}\subseteq {\text{float}}} the relation list ( int ) ⊆ list ( float ) {\displaystyle {\text{list}}({\text{int}})\subseteq {\text{list}}({\text{float}})}

216-391: A subsort of another sort s 2 {\displaystyle s_{2}} , usually by writing s 1 ⊆ s 2 {\displaystyle s_{1}\subseteq s_{2}} or similar syntax. In the above biology example, it is desirable to declare and so on; cf. picture. Wherever a term of some sort s {\displaystyle s}

243-424: A term declaration like ∀ i : int . ( i + i ) : even {\displaystyle \forall i:{\text{int}}.\;(i+i):{\text{even}}} allows to declare a property of integer addition that could not be expressed by ordinary overloading. Early papers on many-sorted logic include: Abstract algebraic logic In mathematical logic , abstract algebraic logic

270-479: A well established subfield of algebraic logic, with many deep and interesting results. These results explain many properties of different classes of logical systems previously explained only on a case-by-case basis or shrouded in mystery. Perhaps the most important achievement of abstract algebraic logic has been the classification of propositional logics in a hierarchy , called the abstract algebraic hierarchy or Leibniz hierarchy, whose different levels roughly reflect

297-438: Is automatically inferred, meaning that each list of integers is also a list of floats. Schmidt-Schauß generalized order-sorted logic to allow for term declarations. As an example, assuming subsort declarations even ⊆ int {\displaystyle {\text{even}}\subseteq {\text{int}}} and odd ⊆ int {\displaystyle {\text{odd}}\subseteq {\text{int}}} ,

SECTION 10

#1732772684175

324-686: Is called function overloading , similar to overloading in programming languages . Order-sorted logic can be translated into unsorted logic, using a unary predicate p i ( x ) {\displaystyle p_{i}(x)} for each sort s i {\displaystyle s_{i}} , and an axiom ∀ x ( p i ( x ) → p j ( x ) ) {\displaystyle \forall x(p_{i}(x)\rightarrow p_{j}(x))} for each subsort declaration s i ⊆ s j {\displaystyle s_{i}\subseteq s_{j}} . The reverse approach

351-478: Is required, a term of any subsort of s {\displaystyle s} may be supplied instead ( Liskov substitution principle ). For example, assuming a function declaration mother : animal ⟶ animal {\displaystyle {\text{mother}}:{\text{animal}}\longrightarrow {\text{animal}}} , and a constant declaration lassie : dog {\displaystyle {\text{lassie}}:{\text{dog}}} ,

378-574: 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 . Many-sorted logic Many-sorted logic can reflect formally our intention not to handle

405-482: Is the study of the algebraization of deductive systems arising as an abstraction of the well-known Lindenbaum–Tarski algebra , and how the resulting algebras are related to logical systems. The archetypal association of this kind, one fundamental to the historical origins of algebraic logic and lying at the heart of all subsequently developed subtheories, is the association between the class of Boolean algebras and classical propositional calculus . This association

432-643: The 1950s and 60s with the work of Helena Rasiowa , Roman Sikorski , Jerzy Łoś , and Roman Suszko (to name but a few). It reached maturity in the 1980s with the seminal publications of the Polish logician Janusz Czelakowski , the Dutch logician Wim Blok and the American logician Don Pigozzi . The focus of abstract algebraic logic shifted from the study of specific classes of algebras associated with specific logical systems (the focus of classical algebraic logic), to

459-418: The development of abstract algebraic logic are closely connected to (1) and (3) above. With respect to (1), a critical step in the transition was initiated by the work of Rasiowa. Her goal was to abstract results and methods known to hold for the classical propositional calculus and Boolean algebras and some other closely related logical systems, in such a way that these results and methods could be applied to

486-593: The equation x 1 = ? x 2 {\displaystyle x_{1}{\stackrel {?}{=}}\,x_{2}} has the solution { x 1 = x , x 2 = x } {\displaystyle \{x_{1}=x,\;x_{2}=x\}} , where x : s 1 ∩ s 2 {\displaystyle x:s_{1}\cap s_{2}} . Smolka generalized order-sorted logic to allow for parametric polymorphism . In his framework, subsort declarations are propagated to complex type expressions. As

513-440: The intention mentioned above; a many-sorted logic is any package of information which fulfils it. In most cases, the following are given: The domain of discourse of any structure of that signature is then fragmented into disjoint subsets, one for every sort. When reasoning about biological organisms, it is useful to distinguish two sorts: p l a n t {\displaystyle \mathrm {plant} } and

540-487: The properties of specific classes of algebras used to "algebraize" specific logical systems of particular interest to specific logical investigations. Generally, the algebra associated with a logical system was found to be a type of lattice , possibly enriched with one or more unary operations other than lattice complementation . Abstract algebraic logic is a modern subarea of algebraic logic that emerged in Poland during

567-473: 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

SECTION 20

#1732772684175

594-399: The strength of the ties between a logic at a particular level and its associated class of algebras. The position of a logic in this hierarchy determines the extent to which that logic may be studied using known algebraic methods and techniques. Once a logic is assigned to a level of this hierarchy, one may draw on the powerful arsenal of results, accumulated over the past 30-odd years, governing

621-404: The study of: The passage from classical algebraic logic to abstract algebraic logic may be compared to the passage from "modern" or abstract algebra (i.e., the study of groups , rings , modules , fields , etc.) to universal algebra (the study of classes of algebras of arbitrary similarity types (algebraic signatures ) satisfying specific abstract properties). The two main motivations for

648-494: The term mother ( lassie ) {\displaystyle {\text{mother}}({\text{lassie}})} is perfectly valid and has the sort animal {\displaystyle {\text{animal}}} . In order to supply the information that the mother of a dog is a dog in turn, another declaration mother : dog ⟶ dog {\displaystyle {\text{mother}}:{\text{dog}}\longrightarrow {\text{dog}}} may be issued; this

675-418: The universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming . Both functional and assertive " parts of speech " in the language of the logic reflect this typeful partitioning of the universe, even on the syntax level: substitution and argument passing can be done only accordingly, respecting the "sorts". There are various ways to formalize

702-753: Was discovered by George Boole in the 1850s, and then further developed and refined by others, especially C. S. Peirce and Ernst Schröder , from the 1870s to the 1890s. This work culminated in Lindenbaum–Tarski algebras , devised by Alfred Tarski and his student Adolf Lindenbaum in the 1930s. Later, Tarski and his American students (whose ranks include Don Pigozzi) went on to discover cylindric algebra , whose representable instances algebraize all of classical first-order logic , and revived relation algebra , whose models include all well-known axiomatic set theories . Classical algebraic logic, which comprises all work in algebraic logic until about 1960, studied

729-983: Was successful in automated theorem proving: in 1985, Christoph Walther could solve a then benchmark problem by translating it into order-sorted logic, thereby boiling it down an order of magnitude, as many unary predicates turned into sorts. In order to incorporate order-sorted logic into a clause-based automated theorem prover, a corresponding order-sorted unification algorithm is necessary, which requires for any two declared sorts s 1 , s 2 {\displaystyle s_{1},s_{2}} their intersection s 1 ∩ s 2 {\displaystyle s_{1}\cap s_{2}} to be declared, too: if x 1 {\displaystyle x_{1}} and x 2 {\displaystyle x_{2}} are variables of sort s 1 {\displaystyle s_{1}} and s 2 {\displaystyle s_{2}} , respectively,

#174825