128.151.32.169: /* Single electron motion */

2014-01-29T01:51:13Z

Single electron motion

New page

{{technical|date=July 2013}}
'''Many-sorted logic''' can reflect formally our intention not to handle 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 "[[Lexical category|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 more ways to formalize the intention mentioned above; a ''many-sorted logic'' is any package of information which fulfills it. In most cases, the following are given:
* a set of sorts, ''S''
* an [[Signature (logic)#Many-sorted signatures|appropriate generalization]] of the notion of ''[[Signature (logic)|signature]]'' to be able to handle the additional information that comes with the sorts.
The [[domain of discourse]] of any [[structure (mathematical logic)|structure]] of that signature is then fragmented into disjoint subsets, one for every sort.

==Example==
When reasoning about biological creatures, it is useful to distinguish two sorts: <math>\textit{plant}</math> and <math>\textit{animal}</math>. While a function <math>\textit{mother}: \textit{animal} \longrightarrow \textit{animal}</math> makes sense, a similar function <math>\textit{mother}: \textit{plant} \longrightarrow \textit{plant}</math> usually does not. Many-sorted logic allows one to have terms like <math>\textit{mother}(\textit{lassie})</math>, but to discard terms like <math>\textit{mother}(\textit{my\_favorite\_oak})</math> as syntactically ill-formed.

== Algebraization ==

The algebraization of many-sorted logic is explained in an article by Caleiro and Gonçalves,<ref>{{cite book| author=Carlos Caleiro, Ricardo Gonçalves| chapter=On the algebraization of many-sorted logics| title=Proc. 18th int. conf. on Recent trends in algebraic development techniques (WADT)| year=2006| volume=| pages=21–36| publisher=Springer| editor=| series=| isbn=978-3-540-71997-7| url=http://sqig.math.ist.utl.pt/pub/CaleiroC/06-CG-manysorted.pdf}}</ref> which generalizes [[abstract algebraic logic]] to the many-sorted case, but can also be used as introductory material.

==Order-sorted logic==
While ''many-sorted'' logic requires two distinct sorts to have disjoint universe sets, ''order-sorted'' logic allows one sort <math>s_1</math> to be declared a subsort of another sort <math>s_2</math>, usually by writing <math>s_1 \subseteq s_2</math> or similar syntax. In the [[#example|above example]], it is desirable to declare
:<math>\textit{dog} \subseteq \textit{carnivore}</math>,
:<math>\textit{dog} \subseteq \textit{mammal}</math>,
:<math>\textit{carnivore} \subseteq \textit{animal}</math>,
:<math>\textit{mammal} \subseteq \textit{animal}</math>,
:<math>\textit{animal} \subseteq \textit{creature}</math>,
:<math>\textit{plant} \subseteq \textit{creature}</math>,
and so on.

Wherever a term of some sort <math>s</math> is required, a term of any subsort of <math>s</math> may be supplied instead. For example, assuming a function declaration <math>\textit{mother}: \textit{animal} \longrightarrow \textit{animal}</math>, and a constant declaration <math>\textit{lassie}: \textit{dog}</math>, the term <math>\textit{mother}(\textit{lassie})</math> is perfectly valid and has the sort <math>\textit{animal}</math>. In order to supply the information that the mother of a dog is a dog in turn, another declaration <math>\textit{mother}: \textit{dog} \longrightarrow \textit{dog}</math> may be issued; this is called ''function overloading'', similar to [[Overloading (programming)|overloading in programming languages]].

Order-sorted logic can be translated into unsorted logic, using a unary predicate <math>p_i(x)</math> for each sort <math>s_i</math>, and an axiom <math>\forall x: p_i(x) \rightarrow p_j(x)</math> for each subsort declaration <math>s_i \subseteq s_j</math>. The reverse approach 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.<ref>{{cite journal|first1=Christoph|last1=Walther|title=A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution|journal=Artif. Intell.|volume=26|number=2|pages=217–224|url=http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf|year=1985}}</ref>

In order to incorporate order-sorted logic into a clause-based automated theorem prover, a corresponding ''order-sorted [[unification (computer science)|unification]]'' algorithm is necessary, which requires for any two declared sorts <math>s_1, s_2</math> their intersection <math>s_1 \cap s_2</math> to be declared, too: if <math>x_1</math> and <math>x_2</math> is a variable of sort <math>s_1</math> and <math>s_2</math>, respectively, the equation <math>x_1 \stackrel{?}{=} x_2</math> has the solution <math>\{ x_1 = x, \; x_2 = x\}</math>, where <math>x: s_1 \cap s_2</math>.

Smolka generalized order-sorted logic to allow for [[parametric polymorphism]].
<ref>{{cite conference|first1=Gert|last1=Smolka|title=Logic Programming with Polymorphically Order-Sorted Types|booktitle=Int. Workshop Algebraic and Logic Programming|publisher=Springer|series=LNCS|volume=343|pages=53–70|date=Nov 1988}}</ref><ref>{{citation|first1=Gert|last1=Smolka|title=Logic Programming over Polymorphically Order-Sorted Types|publisher=Univ. Kaiserslautern, Germany|date=May 1989}}</ref>
In his framework, subsort declarations are propagated to complex type expressions.
As a programming example, a parametric sort <math>\textit{list}(X)</math> may be declared (with <math>X</math> being a type parameter as in a [[Template (C++)#Function templates|C++ template]]), and from a subsort declaration <math>\textit{int} \subseteq \textit{float}</math> the relation <math>\textit{list}(\textit{int}) \subseteq \textit{list}(\textit{float})</math> 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.<ref>{{cite book|first1=Manfred|last1=Schmidt-Schauß|title=Computational Aspects of an Order-Sorted Logic with Term Declarations|publisher=Springer|series=LNAI|volume=395|date=Apr 1988}}</ref>
As an example, assuming subsort declarations <math>\textit{even} \subseteq \textit{int}</math> and <math>\textit{odd} \subseteq \textit{int}</math>, a term declaration like <math>\forall i:\textit{int}. \; (i+i):\textit{even}</math> allows to declare a property of integer addition that could not be expressed by ordinary overloading.

== See also ==
{{Portal|Logic}}

* [[Categorical logic]]
* [[Many-sorted first-order logic#Many-sorted logic]]

== References ==
{{reflist}}
Early papers on many-sorted logic include:
* {{cite journal| author=Gilmore, P.C.| title=An addition to "Logic of many-sorted theories"| journal=Compositio Mathematica| year=1958| volume=13| pages=277–281| url=http://archive.numdam.org/article/CM_1956-1958__13__277_0.pdf}}
* {{cite journal| author=A. Oberschelp| title=Untersuchungen zur mehrsortigen Quantorenlogik| journal=Mathematische Annalen| year=1962| volume=145| number=4| pages=297–333| url=http://gdz.sub.uni-goettingen.de/index.php?id=11&L=4&PPN=GDZPPN002289989&L=1}}
* {{cite journal| author=F. Jeffry Pelletier| title=Sortal Quantification and Restricted Quantification| journal=Philosophical Studies| year=1972| volume=23| pages=400–404| url=http://www.sfu.ca/~jeffpell/papers/SortalRestrQuant.pdf}}

== External links ==
* [http://react.cs.uni-sb.de/teaching/decision-procedures-verification-06/ch01.pdf "Many-sorted Logic"], the first chapter in [http://react.cs.uni-sb.de/~zarba/notes.html ''Lecture Notes on Decision Procedures''] by [http://react.cs.uni-sb.de/~zarba/ Calogero G. Zarba]

[[Category:Systems of formal logic]]

Polywell - Revision history

128.151.32.169: /* Single electron motion */