View source for Logic translation

{{short description|Translation of a text into a logical system}}
{{good article}}
{{Use dmy dates|date=March 2023}}
[[File:Example formalization.svg|thumb|upright=1.5|alt=Visualization of how to translate an English sentence into first-order logic|Translation of an English sentence to first-order logic]]

'''Logic translation''' is the process of representing a text in the [[formal language]] of a [[Logic#Systems of logic|logical system]]. If the original text is formulated in [[Natural language|ordinary language]] then the term '''natural language formalization''' is often used. An example is the translation of the English sentence "some men are bald" into [[first-order logic]] as {{nowrap|<math>\exist x (M(x) \land B(x))</math>}}.{{efn|In first-order logic notation, <math>\exist</math> indicates that some element exists. Uppercase letters like <math>M</math> and <math>B</math> are used as predicates to express ideas like ''man'' or ''bald''. The symbol <math>\land</math> indicates a conjunction, meaning that both predicates apply.}} The purpose is to reveal the [[Logical form|logical structure]] of [[argument]]s. This makes it possible to use the precise rules of formal logic to assess whether these arguments are correct. It can also guide [[Logical reasoning|reasoning]] by arriving at new [[Consequent|conclusions]]. 

Many of the difficulties of the process are caused by [[Vagueness|vague]] or [[Ambiguity|ambiguous]] expressions in natural language. For example, the English word "is" can mean that something [[existence|exists]], that it is [[Identity (philosophy)|identical]] to something else, or that it has a certain [[Property (philosophy)|property]]. This contrasts with the precise nature of formal logic, which avoids such ambiguities. Natural language formalization is relevant to various fields in the [[sciences]] and [[humanities]]. It may play a key role for [[logic]] in general since it is needed to establish a link between many forms of reasoning and abstract logical systems. The use of [[informal logic]] is an alternative to formalization since it analyzes the cogency of ordinary language arguments in their original form. Natural language formalization is distinguished from logic translations that convert formulas from one logical system into another, for example, from [[modal logic]] to first-order logic. This form of logic translation is specifically relevant for [[logic programming]] and [[metalogic]].

A major challenge in logic translation is determining the accuracy of translations and separating good from bad ones. The technical term for this is ''criteria of adequate translations''. An often-cited criterion states that translations should preserve the [[inference|inferential]] relations between sentences. This implies that if an argument is [[Validity (logic)|valid]] in the original text then the translated argument should also be valid. Another criterion is that the original sentence and the translation have the same [[truth condition]]s. Further suggested conditions are that a translation does not include additional or unnecessary symbols and that its grammatical structure is similar to the original sentence. Various procedures for translating texts have been suggested. Preparatory steps include understanding the meaning of the original text and [[Paraphrase|paraphrasing]] it to remove ambiguities and make its logical structure more explicit. As an intermediary step, a translation may happen into a hybrid language. This hybrid language implements a logical formalism but retains the vocabulary of the original expression. In the last step, this vocabulary is replaced by logical symbols. Translation procedures are usually not exact algorithms and their application depends on intuitive understanding. Logic translations are often criticized on the grounds that they are unable to accurately represent all the aspects and nuances of the original text.

== Definition ==
A logic translation is a [[translation]] of a text into a [[Logic#Systems of logic|logical system]]. For example, translating the sentence "all skyscrapers are tall" as <math>\forall x (S(x) \to T(x))</math> is a logic translation that expresses an English language sentence in the logical system known as [[first-order logic]]. The aim of logic translations is usually to make the [[Logical form|logical structure]] of [[natural language]] [[argument]]s explicit. This way, the rules of [[formal logic]] can be used to assess whether the arguments are [[Validity (logic)|valid]].<ref>{{multiref | {{harvnb|Hurley|2018|p=260, 473}} | {{harvnb|Brun|2003|p=83, 175-7, 207}} | {{harvnb|Baumgartner|Lampert|2008|p=93-4}} }}</ref>

Understood in a wide sense, a translation is a process that associates expressions belonging to a [[Translation#Source and target languages|source language]] with expressions belonging to a target language.<ref>{{multiref | {{harvnb|Saule|Aisulu|2014|p=122}} | {{harvnb|Brun|2003|p=176}} }}</ref> For example, in a sentence-by-sentence translation of an English text into French, English sentences are linked to their French counterparts. The hallmark of logic translations is that the target language belongs to a logical system.<ref name="auto3">{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2900}} | {{harvnb|Brun|2003|p=177}} | {{harvnb|Hintikka|2023}} }}</ref> Logic translations differ from regular translations in that they are mainly concerned with expressing the logical structure of the original text and less with its concrete content. Regular translations, on the other hand, take various additional factors into account pertaining to the content, meaning, and style of the original expression.<ref>{{multiref | {{harvnb|Brun|2003|p=111-2, 176-7}} | {{harvnb|Peregrin|Svoboda|2016|p=58-9}} }}</ref> For this reason, some theorists, like Peregrin and Svoboda,  have argued that it is not a form of translation. They tend to use other terms, such as "formalization", "symbolization", and "explication".<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2016|p=59}} | {{harvnb|Brun|2003|p=175, 177, 180}} | {{harvnb|Magnus|Button|Thomas-Bolduc|Zach|2021|p=73-4, 259-60}} }}</ref> This opinion is not shared by all logicians and some, like [[Richard Mark Sainsbury|Mark Sainsbury]], argue that successful logic translations preserve all the original meaning while making the logical structure explicit.<ref>{{multiref | {{harvnb|Baumgartner|Lampert|2008|p=98-9}} | {{harvnb|Peregrin|Svoboda|2016|p=59}} }}</ref>

Discussions on logic translations usually focus on the problem of expressing the logical structure of ordinary language sentences in a formal logical system. The term also covers cases where the translation happens from one logical system into another.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2900}} | {{harvnb|Causey|1980|p=373–374}} | {{harvnb|Mossakowski|Diaconescu|Tarlecki|2009|p=95}} }}</ref>

== Basic concepts ==
{{see also|Logic#Basic concepts}}
[[File:Modus ponendo ponens.png|thumb|alt=Depiction of inference using modus ponens|Through logic translation it is possible to evaluate whether ordinary language arguments follow a valid rule of inference, like [[modus ponens]].]]
Various basic concepts are employed in the study and analysis of logic translations. [[Logic]] is interested in correct reasoning, which happens in the form of [[inference]]s or arguments. An argument is a set of [[premise]]s together with a conclusion.<ref>{{multiref | {{harvnb|Blackburn|2008|loc=[https://www.oxfordreference.com/view/10.1093/oi/authority.20110803095423356 argument]}} | {{harvnb|Stairs|2017|p=[https://books.google.com/books?id=Km1QDwAAQBAJ&pg=PA343 343]}} | {{harvnb|Mossakowski|Diaconescu|Tarlecki|2009|p=95}} }}</ref> An argument is [[Deductive reasoning|deductively]] valid if it is impossible for its conclusion to be false if all its premises are true.<ref>{{harvnb|Turetzky|2019|p=[https://books.google.com/books?id=Xka6DwAAQBAJ&pg=PA35 35]}}</ref> Valid arguments follow a [[rule of inference]], which prescribes how the premises and the conclusion have to be structured.<ref>{{multiref | {{harvnb|Byrne|Evans|Newstead|2019|p=[https://books.google.com/books?id=5R6eDwAAQBAJ&pg=PT59 59]}} | {{harvnb|Dowden|2020|p=392}} | {{harvnb|Jamieson|2013|p=[https://books.google.com/books?id=GplfBgAAQBAJ&pg=PA34 34]}} }}</ref> A prominent rule of inference is [[modus ponens]], which states that arguments of the form "(1) ''p''; (2) if ''p'' then ''q''; (3) therefore ''q''" are valid.<ref>{{multiref | {{harvnb|Blackburn|2016|p=[https://www.oxfordreference.com/view/10.1093/oi/authority.20110803100432990 422]|loc=rule of inference}} | {{harvnb|Franks|Therriault|Buhr|Chiang|2013|p=146}} }}</ref> An example of an argument following modus ponens is: "(1) today is Sunday; (2) if today is Sunday then I don't have to go to work today; (3) therefore I don't have to go to work today".<ref>{{harvnb|Velleman|2006|p=[https://books.google.com/books?id=lptwaMuAtBAC&pg=PA8 8, 103]}}</ref>

There are different logical systems for assessing which arguments are valid.<ref>{{multiref | {{harvnb|Groat|Wang|2002|p=[https://books.google.com/books?id=21Uz_E0HNR4C&pg=PA283 283]}} | {{harvnb|Yaqub|2014|p=[https://books.google.com/books?id=4M6rBAAAQBAJ&pg=PA87 87]}} }}</ref> For example, [[propositional logic]] only focuses on inferences based on [[logical connective]]s, like "and" or "if...then". First-order logic, on the other hand, also includes inferential patterns belonging to expressions like "every" or "some". Extended logics cover further inferences, for example, in relation to what is possible and necessary or regarding temporal relations.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2915}} | {{harvnb|Borchert|2006|loc=[https://philpapers.org/rec/BORMEO Logic, Non-Classical]}} }}</ref>

This means that logical systems usually do not capture all inferential patterns. This is relevant for logic translation since they may miss patterns for which they were not intended. For example, propositional logic can be used to show that the following ordinary language argument is correct: "(1) John is not a pilot; (2) John is a pilot or Bill is a poet; (3) therefore Bill is a poet". However, it fails to show that the argument "(1) John is a pilot; (2) therefore John can aviate" is correct since it is unable to capture the inferential relation between the terms "Pilot" and "can aviate".<ref>{{harvnb|Peregrin|Svoboda|2013|p=2915-6}}</ref> If a logical system is applied to cases beyond its limited scope, it is unable to assess the validity of natural language arguments. The advantage of this limitation is that the [[vagueness]] and [[ambiguity]] of natural language arguments are avoided by making some of the inferential patterns very clear.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2916-7}} | {{harvnb|Hurley|2018|p=260}} }}</ref>

Formal logical systems use precise [[formal language]]s to express their formulas and inferences. In the case of propositional logic, letters like <math>A</math> and <math>B</math> are used to represent simple propositions. They can be combined into more complex propositions using propositional connectives like <math>\land</math> to express that both propositions are true and <math>\lor</math> to express that at least one of the propositions is true. So if <math>A</math> stands for "Adam is athletic" and <math>B</math> stands for "Barbara is athletic", then the formula <math>A \land B</math> represents the claim that "Adam is athletic, and also Barbara is athletic".<ref>{{multiref | {{harvnb|Magnus|Button|Thomas-Bolduc|Zach|2021|p=32-5}} | {{harvnb|Hurley|2018|p=327-31}} }}</ref> First-order logic also includes propositional connectives but introduces additional symbols. Uppercase letters are used for predicates and lowercase letters stand for individuals. For example, if <math>A</math> stands for the predicate "is angry" and <math>e</math> represents the individual Elsa, then the formula <math>A(e)</math> expresses the proposition "Elsa is angry". Another innovation of first-order logic is the use of quantifiers like <math>\exists</math> and <math>\forall</math> to represent the meanings of terms like "some" and "all".<ref>{{multiref | {{harvnb|Magnus|Button|Thomas-Bolduc|Zach|2021|p=191-9}} | {{harvnb|Hurley|2018|p=470-5}} }}</ref>

== Types ==
Logic translations can be classified based on the source language of the original text. For many logic translations, the original text belongs to a natural language, like English or French. In this case, the term "natural language formalization" is often used.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2900}} | {{harvnb|Magnus|Button|Thomas-Bolduc|Zach|2021|p=73-4, 259-60}} | {{harvnb|Brun|2003|p=175, 177}} }}</ref> For example, the sentence "Dana is a logician and Dana is a nice person" can be formalized into propositional logic using the [[logical formula]] <math>L \land N</math>.<ref>{{harvnb|Magnus|Button|Thomas-Bolduc|Zach|2021|p=73-4}}</ref> A further type of logic translation happens between two logical systems. This means that the source text is composed of logical formulas belonging to one logical system and the goal is to associate them with logical formulas belonging to another logical system.<ref>{{multiref | {{harvnb|Mossakowski|Diaconescu|Tarlecki|2009|p=95}} | {{harvnb|Fu|Kutz|2012|p=289}} }}</ref> For example, the formula <math>\Box A(x)</math> in [[modal logic]] can be translated into first-order logic using the formula <math>\forall y (R(x,y) \to A(y))</math>.<ref>{{harvnb|Garson|2023}}</ref>

=== Natural language formalization ===
[[File:Natural language formalization.svg|thumb|upright=1.5|alt=Diagram showing the translation of a full argument|To assess the validity of an ordinary language argument, each of its statements can be translated into a logical system.<ref>{{harvnb|Brun|2003|p=56}}</ref>]]

Natural language formalization is a form of [[semantic parsing]]{{efn|Semantic parsing is the process of finding a formal meaning representation of a natural language sentence. This representation is not restricted to logical reasoning and may serve other purposes as well, such as [[machine translation]]s of one natural language into another.<ref>{{multiref | {{harvnb|Gelbukh|2007|p=[https://books.google.com/books?id=uo0BKcI-qm0C&pg=PA311 311]}} | {{harvnb|Quesada|Mateos|Lopez-Soto|2016|p=[https://books.google.com/books?id=JVEWDAAAQBAJ&pg=PA14 14]}} }}</ref>}} that starts with a sentence in natural language and translates it into a logical formula.<ref name="auto3"/> Its goal is to make the logical structure of natural language sentences and arguments explicit.<ref>{{multiref | {{harvnb|Brun|2003|p=83, 175, 207}} | {{harvnb|Peregrin|Svoboda|2016|p=64}} }}</ref> It is mainly concerned with their logical form while their specific content is usually ignored.<ref>{{multiref | {{harvnb|Brun|2003|p=111-2}} | {{harvnb|Peregrin|Svoboda|2016|p=68}} }}</ref> Logical analysis is a closely related term that refers to the process of uncovering the logical form or structure of a sentence.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2898-9}} | {{harvnb|Colman|2009|loc=[https://www.oxfordreference.com/display/10.1093/oi/authority.20110803100112564;jsessionid=9E8800D02D072B638EDB50ADBDF15026 logical analysis]}} }}</ref> Natural language formalization makes it possible to use formal logic to analyze and evaluate natural language arguments. This is especially relevant for complex arguments, which are often difficult to evaluate without formal tools. Logic translation can also be used to look for new arguments and thereby guide the reasoning process.<ref>{{multiref2 |1={{harvnb|Brun|2003|p=83, 175, 207}} |2={{harvnb|Hintikka|2023}} |3={{harvnb|Baumgartner|Lampert|2008|p=94}} |4={{harvnb|Peregrin|Svoboda|2016|p=55}} }}</ref> The reverse process of formalization is sometimes called "verbalization". It happens when logical formulas are translated back into natural language. This process is less nuanced and discussions concerning the relation between natural language and logic usually focus on the problem of formalization.<ref>{{harvnb|Peregrin|Svoboda|2013|p=2900, 2913}}</ref> 

The success of applications of formal logic to natural language requires that the translation is correct.<ref>{{harvnb|Brun|2003|p=18}}</ref> A formalization is correct if its explicit logical features fit the implicit logical features of the original sentence.<ref name="auto1">{{harvnb|Peregrin|Svoboda|2016|p=63}}</ref> The logical form of ordinary language sentences is often not obvious since there are many differences between natural languages and the formal languages used by logicians.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2897}} | {{harvnb|Hurley|2018|p=327}} }}</ref> This poses various difficulties for formalization. For example, ordinary expressions frequently include vague and ambiguous expressions. For this reason, the validity of an argument often depends not just on the expressions themselves but also on how they are interpreted.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2916-7}} | {{harvnb|Hurley|2018|p=260}} | {{harvnb|Hansson|Hendricks|2018|p=[https://books.google.com/books?id=bs10DwAAQBAJ&pg=PA61 61]}} }}</ref> For example, the sentence "donkeys have ears" could mean that ''all donkeys (without exception) have ears'' or that ''donkeys typically have ears''. The second translation does not exclude the existence of some donkeys without ears. This difference matters for whether a [[universal quantifier]] can be used to translate the sentence. Such ambiguities are not found in the precise formulations of artificial logical languages and have to be solved before translation is possible.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2016|p=62}} | {{harvnb|Bunt|Muskens|Thijsse|2012|p=[https://books.google.com/books?id=LoJyBgAAQBAJ&pg=PT15 15]}} }}</ref>

The problem of natural language formalization has various implications for the [[sciences]] and [[humanities]], especially for the fields of [[linguistics]], [[cognitive science]], and [[computer science]].<ref>{{multiref | {{harvnb|Rabe|2008|p=3}} | {{harvnb|Brun|2003|p=22}} | {{harvnb|Peregrin|Svoboda|2016|p=55}} }}</ref> In the field of [[formal linguistics]], for example, [[Richard Montague]] provides various suggestions for how to formalize English language expressions in his [[Montague grammar|theory of universal grammar]].<ref>{{multiref | {{harvnb|Brun|2003|p=21}} | {{harvnb|Janssen|Zimmermann|2021}} }}</ref> Formalization is also discussed in the [[philosophy of logic]] in relation to its role in understanding and applying logic.<ref>{{harvnb|Brun|2003|p=17, 19}}</ref> If logic is understood as the theory of valid inferences in general then formalization plays a central role in it since many of these inferences are formulated in ordinary language. Logic translation is needed to link formal systems of logic to arguments expressed in ordinary language.<ref>{{multiref | {{harvnb|Brun|2003|p=59}} | {{harvnb|Peregrin|Svoboda|2013|p=2898}} | {{harvnb|Peregrin|Svoboda|2016|p=56}} }}</ref> A related claim is that all logical languages, including highly abstract ones like modal logic and [[many-valued logic]], have to be "anchored in the structures of natural language".<ref>{{harvnb|Peregrin|Svoboda|2013|p=2897-8}}</ref> One difficulty in this regard is that logic is usually understood as a [[formal science]], but a theory of its relation to empirical matters pertaining to ordinary languages goes beyond this purely formal conception.<ref>{{harvnb|Brun|2003|p=59-60}}</ref> For this reason, some theorists like Georg Brun identify a pure branch of logic and contrast it with applied logic, which includes the problem of formalization.<ref>{{harvnb|Brun|2003|p=59-60, 66}}</ref>

Some theorists draw the conclusion from these considerations that informal reasoning takes precedence over formal reasoning. This would imply that formal logic can only succeed if it is based on correct formalization.<ref>{{multiref | {{harvnb|Baumgartner|Lampert|2008|p=93, 113-4}} | {{harvnb|Peregrin|Svoboda|2013|p=2924}} | {{harvnb|Brun|2003|p=83, 175, 207}} }}</ref> For example, Michael Baumgartner and Timm Lampert hold that "there are no [[informal fallacies]]" but only "misunderstanding of informal arguments expressed by inadequate formalizations".<ref>{{harvnb|Baumgartner|Lampert|2008|p=113-4}}</ref> This position is rejected by Jaroslav Peregrin and Vladimír Svoboda, who argue that informal reasoning is not always accurate and may be corrected through the application of formal logic.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2016|p=77-8}} | {{harvnb|Peregrin|Svoboda|2013|p=2924}} }}</ref>

An alternative to formalization is to use [[informal logic]], which analyzes the cogency of natural language arguments in their original form. This has many advantages by avoiding the difficulties associated with logic translations but it also comes with various drawbacks. For example, informal logic lacks the precision found in formal logic for distinguishing between good arguments and [[fallacies]].<ref>{{multiref2 |1={{harvnb|Blair|Johnson|2000|p=[https://philpapers.org/rec/BLAILA-3 93–107]}} |2={{harvnb|Walton|1987|p=[https://philpapers.org/rec/WALIFT 1–32]|loc=1. A new model of argument}} |3={{harvnb|Engel|1982|p=[https://philpapers.org/rec/ENGWGR 59–92]|loc=2. The medium of language}} |4={{harvnb|Craig|1996|loc=[https://philpapers.org/rec/BEAREO Formal and informal logic]}} }}</ref>

==== Examples ====
For [[propositional logic]], the sentence "Tiffany sells jewelry, and Gucci sells cologne" can be translated as <math>T \land G</math>. In this example, <math>T</math> represents the claim "Tiffany sells jewelry", <math>G</math> stands for "Gucci sells cologne", and <math>\land</math> is the logical conjunction corresponding to "and". Another example is the sentence "Notre Dame raises tuition if Purdue does", which can be formalized as <math>P \to N</math>.<ref>{{harvnb|Hurley|2018|p=330}}</ref>

For [[predicate logic]], the sentence "Ann loves Ben" can be translated as <math>L(a, b)</math>. In this example, <math>L</math> stands for "loves", <math>a</math> stands for Ann and <math>b</math> stands for Ben.<ref>{{harvnb|Magnus|Button|Thomas-Bolduc|Zach|2021|p=262}}</ref> Other examples are "some men are bald" as <math>\exist x (M(x) \land B(x))</math>,<ref>{{harvnb|Garrett|2011|p=[https://books.google.com/books?id=qTmJrtBX-ZkC&pg=PA28 28]}}</ref> "all rivers have a head" as <math>\forall x (R(x) \to H(x))</math>,<ref>{{harvnb|Baumgartner|Lampert|2008|p=98}}</ref> "no frogs are birds" as <math>\forall x (F(x) \to \lnot B(x))</math>,<ref>{{harvnb|Hurley|2018|p=473}}</ref> and "if Elizabeth is a historian, then some women are historians" as <math>H(e) \to \exists x (W(x) \land H(x))</math>.<ref>{{harvnb|Hurley|2018|p=477}}</ref>

==== Problematic expressions ====
For various natural language expressions, it is not clear how they should be translated and the right translation may differ from case to case. The vagueness and ambiguity of ordinary language, in contrast to the precise nature of logic, is often responsible for these problems. For this reason, it has proven difficult to find a general [[algorithm]] to cover all cases of translation.<ref>{{multiref | {{harvnb|Hurley|2018|p=327-8}} | {{harvnb|Baumgartner|Lampert|2008|p=95}} }}</ref>  For example, the meaning of basic English expressions like "and", "or", and "if...then" can vary from context to context. The corresponding logical operators in symbolic logic (<math>\land</math>, <math>\lor</math>, <math>\to</math>), on the other hand, have very precisely defined meanings. In this regard, they only capture some aspects of the original meaning.<ref>{{harvnb|Hurley|2018|p=327-8}}</ref>

The English word "is" poses another such difficulty since it has many meanings. It can express [[existence]] (as in "there is a Santa Claus"), [[Identity (philosophy)|identity]] (as in "Superman is Clark Kent"), and [[Predication (philosophy)|predication]] (as in "Venus is a planet"). Each one of these meanings is expressed differently in logical systems like first-order logic.<ref>{{harvnb|Hintikka|2023}}</ref> Another difficulty is that [[Quantifier (logic)|quantifiers]] are often not explicitly expressed in ordinary language. For example, the sentence "emeralds are green" does not directly state the universal quantifier "all", i.e. "all emeralds are green". However, some sentences with a similar structure, such as the "children live next door", imply the [[existential quantifier]] "some", i.e. "some children live next door".<ref>{{harvnb|Hurley|2018|p=263}}</ref>

A closely related problem is found in some valid natural language arguments whose most obvious translations are invalid in formal logic. For example, the argument "(1) Fury is a horse; (2) therefore Fury is an animal" is valid but the corresponding argument in formal logic from <math>H(f)</math> to <math>A(f)</math> is invalid. One solution is to add to the argument an additional premise stating that "all horses are animals". Another is to translate the sentence "Fury is a horse" as <math>H(f) \land A(f)</math>. These solutions come with new problems of their own.<ref>{{harvnb|Brun|2003|p=241}}</ref> Further problematic expressions are [[definite descriptions]], [[conditional sentence]], and [[Adjective#Attributive adjective|attributive adjectives]], as well as [[mass nouns]] and [[Anaphora (linguistics)|anaphora]].<ref>{{harvnb|Brun|2003|p=19}}</ref>

=== Translation between logics ===
A further type of logic translation takes place between logical systems. A translation between two logical systems can be defined in a formal sense as a [[Function (mathematics)|mathematical function]]. This function maps sentences of the first system to sentences of the second system while obeying the [[Logical consequence|entailment relations]] between the original sentences. This means that if a sentence entails another sentence in the first logic, then the translation of the first sentence should entail the translation of the second sentence in the second logic. This way, a translation from one logic to another represents the formulas, proofs, and [[Model (logic)|models]] of the first logic in terms of the second.<ref>{{multiref | {{harvnb|Fu|Kutz|2012|p=290-2}} | {{harvnb|Rabe|2008|p=66}} | {{harvnb|Mossakowski|Diaconescu|Tarlecki|2009|p=97-8}} }}</ref> This is sometimes referred to as ''conservative translation''. It contrasts with ''rough translation'', which only maps the sentences of the first logic to sentences of the second logic without regard to their entailment relations.<ref>{{harvnb|Fu|Kutz|2012|p=291}}</ref>

A preliminary of logic translations is that there is not one logic but many logics.<ref>{{harvnb|Rabe|2008|p=11}}</ref> These logics differ from each other concerning the languages they use as well as the rules of inference they see as valid. For example, [[intuitionistic logic]] differs from [[classical logic]] since it rejects certain rules of inference, such as the [[double negation elimination]]. This rule states that if a sentence is not not true, then it is true, i.e. that <math>A</math> follows from <math>\lnot \lnot A</math>.<ref>{{multiref | {{harvnb|Moschovakis|2022}} | {{harvnb|Borchert|2006|loc=[https://philpapers.org/rec/BORMEO Logic, Non-Classical]}} }}</ref> One way to translate intuitionistic logic into non-intuitionistic logic is by using a [[modal operator]]. This is based on the idea that intuitionistic logic expresses not just what is true but what is [[Knowledge|knowable]]. For example, the formula <math>\lnot p</math> in intuitionistic logic can be translated as <math>K \lnot p</math> where <math>K</math> is a model operator expressing that the following formula is knowable.<ref>{{harvnb|Shapiro|2014|p=[https://books.google.com/books?id=hUKbBAAAQBAJ&pg=PT83 75-6]}}</ref>

Another example is the translation of modal logic to regular predicate logic. Modal logic contains additional symbols for possibility (<math>\diamond</math>) and necessity (<math>\Box</math>) not found in regular predicate logic. One way to translate them is to introduce new predicates, such as the predicate R, which indicates that one [[possible world]] is accessible from another possible world. For example, the modal logic expression <math>\lfloor \diamond p \rfloor _{\iota}</math> (it is possible that ''p'' is true in the actual world) can be translated as <math>\exists v R(\iota, v) \land \lfloor p \rfloor _v</math> (there exists a possible world that is accessible from the actual world and ''p'' is true in it).<ref>{{harvnb|MacNish|Pearce|Pereira|1994|p=[https://books.google.com/books?id=jeNdp3lhmXsC&pg=PA366 366–7]}}</ref>

Translations between logics are relevant for [[metalogic]] and [[logic programming]]. In metalogic, they can be used to study the properties of logical systems and the relations between them.<ref>{{multiref | {{harvnb|Rabe|2008|p=66-8, 99-101}} | {{harvnb|Mossakowski|Diaconescu|Tarlecki|2009|p=95}} }}</ref> In logic programming, they make it possible for programs limited to one type of logic to be applied to many additional cases. With the help of logic translations, programs like [[Prolog]] can be used to solve problems in modal logic and [[temporal logic]] even though Prolog does not natively support these logical systems.<ref>{{multiref | {{harvnb|Dyckhoff|Herre|Schroeder-Heister|1996|p=[https://books.google.com/books?id=9sW3JsG8zIUC&pg=PA21 21, 31–2]}} | {{harvnb|Maher|1996|p=[https://books.google.com/books?id=umj7bcGpr5QC&pg=PA65 65]}} | {{harvnb|Gabbay|Ohlbach|1994|p=[https://books.google.com/books?id=MAlmnK5AZDoC&pg=PA462 462–3]}} }}</ref> A closely related issue concerns the question of how to translate a formal language like [[Attempto Controlled English|Controlled English]] into a logical system. Controlled English is a [[controlled language]] that limits grammar and vocabulary with the goal of reducing ambiguity and complexity. In this regard, the advantage of Controlled English is that every sentence has a unique interpretation. This makes it possible to use algorithms to translate them into formal logic, which is generally not possible for natural languages.<ref>{{multiref2 |1={{harvnb|Pease|Li|2010|p=245-7}} |2={{harvnb|Kuhn|2014|p=152}} |3={{harvnb|Zoya|2016|p=[https://books.google.com/books?id=MJuxDAAAQBAJ&pg=PA77 77]}} }}</ref>

== Criteria of adequate translations ==
Criteria of adequate translations specify how to distinguish good from bad translations. They determine whether a logical formula accurately represents the logical structure of the sentence it translates. This way, they help logicians decide between competing translations of the same sentence.<ref>{{multiref2 |1={{harvnb|Peregrin|Svoboda|2013|p=2897, 2899, 2915}}  |2={{harvnb|Baumgartner|Lampert|2008|p=93}} |3={{harvnb|Peregrin|Svoboda|2016|p=63}} |4={{harvnb|Brun|2003|p=15}} }}</ref> Various criteria are discussed in the academic literature.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2918-9}} | {{harvnb|Baumgartner|Lampert|2008|p=96, 98}} }}</ref> According to various theorists, like Peregrin and Svoboda, the most basic criterion is that translations should preserve the inferential relations between sentences. This principle is sometimes called the ''criterion of syntactic correctness'' or the ''criterion of reliability''.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2899}} | {{harvnb|Baumgartner|Lampert|2008|p=96}} | {{harvnb|Peregrin|Svoboda|2016|p=77}} }}</ref> It stipulates that if an argument is valid in the original text then the translated argument is also valid.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2917}} | {{harvnb|Peregrin|Svoboda|2016|p=68-9, 77}} | {{harvnb|Brun|2003|p=214, 221}} }}</ref> One difficulty in this regard is that the same sentence may form part of several arguments, sometimes as a premise and sometimes as a conclusion. A translation of a sentence is only correct if in all or nearly all these cases, the inferential relations are preserved.<ref>{{harvnb|Peregrin|Svoboda|2013|p=2918-9}}</ref> According to the view of [[holism]], this implies that one cannot evaluate sentence translations individually. This position holds that the correctness of a translation of one sentence depends on how other sentences are translated to ensure correspondence in the inferential relations. This view is rejected by atomists, who claim that the correctness of sentence translations can be assessed individually.<ref>{{harvnb|Peregrin|Svoboda|2013|pp=2899–2900, 2917}}</ref>

A closely related criterion focuses on the truth conditions of sentences.<ref>{{harvnb|Peregrin|Svoboda|2013|p=2899}}</ref> A ''truth condition'' of a sentence is what the world must be like for that sentence to be true.<ref>{{harvnb|Blackburn|2008a|loc=[https://www.oxfordreference.com/display/10.1093/oi/authority.20110803105953851;jsessionid=7B8D604DEBF650724327239FB7E268F8 truth conditions]}}</ref> This criterion states that for adequate translations, the truth conditions of the original sentence are identical to the truth conditions of the translated sentence. The mere fact that the sentence and its translation have the same truth value is not sufficient. Instead, it implies that whenever one is true, the other is also true, i.e. they have to have the same truth value in all possible circumstances.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2899}} | {{harvnb|Baumgartner|Lampert|2008|p=98-100}} | {{harvnb|Brun|2003|p=208, 211}} }}</ref> This criterion is not universally accepted and it has been criticized based on the claim that logical formulas do not have truth conditions. According to this view, the symbols they use are meaningless by themselves and only have the purpose of expressing the logical form of a sentence without implying any concrete content.<ref name="auto1"/> Another problem with this approach is that all [[Tautology (logic)|tautologies]] have the same truth conditions: they are true independently of the circumstances. This would imply that any tautology is a correct translation of any other tautology.<ref>{{harvnb|Brun|2003|p=211}}</ref>

Besides these core criteria, various additional criteria are often discussed in the academic literature. Their goal is usually to exclude bad translations that nonetheless comply with the other criteria. For example, according to the first two criteria, the sentence "it rains" could be formalized as <math>p</math> or as <math>\lnot \lnot \lnot \lnot \lnot \lnot p</math>. The reason is that both formulas have the same truth conditions and the same inferential patterns. However, the second formula is a bad translation. One additional criterion is that translations should not include symbols that do not correspond to expressions in the original sentence. According to it, the translation of "it rains" should not include the symbol for logical negation (<math>\lnot</math>) since a corresponding expression is not found in the original sentence.<ref name="auto2">{{harvnb|Brun|2003|p=235-7, 253-4}}</ref>

Another criterion holds that the order of symbols in the translation should reflect the order of the expressions in the original sentence. For example, the sentence "Pete went up the hill and Quinn went up the hill" should be translated as <math>p \land q</math> and not as <math>q \land p</math>.<ref name="auto2"/> A closely related criterion is the principle of ''transparency'', which states that translations should aim to be similar to the original expression. This concerns, for example, that a translation reflects the grammatical structure of the original sentence as closely as possible.<ref>{{harvnb|Peregrin|Svoboda|2013|p=2918}}</ref> The principle of ''parsimony'' states that simple translations (i.e. logical formulas that use as few symbols as possible) are to be preferred.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2916-9}} | {{harvnb|Brun|2003|p=181}} | {{harvnb|Peregrin|Svoboda|2016|p=69}} }}</ref> One way to test whether a formalization is correct is to translate it back into natural language and see if this second translation matches the original.<ref>{{harvnb|Brun|2003|p=198-9}}</ref>

The problem of the criteria of adequate translations is often not discussed in detail in introductions to logic. One reason for this is that some theorists, like Herbert E. Hendry, see logic translation as an [[The arts|art]] or an intuitive practice. According to this view, it is based on a practical skill learned from [[experience]] with many examples and guided by some rough rules of thumb. This outlook implies that there are no strict rules of adequate formalization. Critics of this idea argue that without clear criteria of adequate translations it is very difficult to decide between competing formalizations of the same sentence.<ref>{{multiref | {{harvnb|Baumgartner|Lampert|2008|p=94}} | {{harvnb|Brun|2003|p=67-8, 195}} | {{harvnb|Otto|Tuedio|2012|p=[https://books.google.com/books?id=3frrCAAAQBAJ&pg=PA315 315]}} }}</ref>

== Translation procedures ==
Various logicians have proposed translation procedures employing several steps to arrive at correct translations. Some only constitute rough guidelines to help translators in the process while others consist of detailed and effective procedures covering all the steps needed to arrive at a translation. In either case, they are usually not exact algorithms that could be blindly followed but rather tools to simplify the process.<ref>{{multiref2 |1={{harvnb|Baumgartner|Lampert|2008|p=94-5}} |2={{harvnb|Hurley|2018|p=260}} |3={{harvnb|Peregrin|Svoboda|2013|p=2911}} |4={{harvnb|Brun|2003|p=197}} }}</ref> 

Preparatory steps may be taken within natural language before the actual translation starts. An initial step is often to understand the meaning of the original text, for example, by analyzing the claims made in it. This includes identifying which arguments are made and whether a claim acts as a premise or as a conclusion.<ref>{{multiref | {{harvnb|Brun|2003|p=17}} | {{harvnb|Hurley|2018|p=260}} | {{harvnb|Causey|1980|p=373–374}} }}</ref> At this stage, a common recommendation is to paraphrase the sentences to make the claims more explicit, remove ambiguities, and highlight their logical structure. For example, the sentence "John Paul II is infallible" could be paraphrased as "it is not the case that John Paul II is fallible".<ref>{{multiref | {{harvnb|Brun|2003|p=195-6}} | {{harvnb|Causey|1980|p=373–374}} }}</ref> This can involve identifying [[truth function|truth-functional]] connectives, like "and", "if...then", or "not", and decomposing the text accordingly. Each of the units analyzed this way is an individual claim that is either true or false.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2901}} | {{harvnb|Baumgartner|Lampert|2008|p=96}} | {{harvnb|Peregrin|Svoboda|2016|p=62-3}} }}</ref> A closely related step is to group the individual expressions into logical units and classify them according to their logical role. In the sentence above, for example, "is fallible" is a predicate and the expression "it is not the case that" corresponds to the logical connective for [[negation]].<ref>{{harvnb|Brun|2003|p=195-6}}</ref>

Once these preparations are done, some theorists, like Peregrin and Svoboda, recommend translation into a hybrid language. Such hybrid expressions already contain a logical formalism but retain regular names for predicates and proper names. For example, the sentence "All rivers have heads" could be translated as <math>\forall x ((River(x)) \to HasHead(x))</math>. The idea behind this step is that the regular terms still carry their original meaning and thereby make it easier to understand the formulas and to see how they relate to the original text. The natural language vocabulary is usually not precisely defined and therefore lacks the exactness demanded by formal logic.<ref>{{multiref | {{harvnb|Peregrin|Svoboda|2013|p=2911-3}} | {{harvnb|Peregrin|Svoboda|2016|p=60-1, 63, 77}} }}</ref> As a last step, these regular terms are then replaced by logical symbols. For the expression above, this would result in the formula <math>\forall x ((R(x)) \to H(x))</math>. This way, the connection to the ordinary language meanings is cut. The formulas become a purely formal expression of the logical structure of the original text and any specific content is removed.<ref>{{multiref | {{harvnb|Causey|1980|p=373–374}} | {{harvnb|Peregrin|Svoboda|2013|p=2913}} | {{harvnb|Peregrin|Svoboda|2016|p=60-1, 63, 77}} }}</ref>

The formalization of a full argument consists in several steps since the argument is made up of several propositions.<ref>{{harvnb|Brun|2003|p=57}}</ref> Once the translation is complete, the formal tools of the logical system, such as its rules of inference, can be employed to assess whether the argument is valid.<ref name="auto">{{harvnb|Brun|2003|p=17-8}}</ref>

== Criticism ==
Criticism of logic translations is primarily focused on the limitations and the range of valid applications, as well as the way they are discussed in academic literature. Logic translation is a widely accepted and utilized process in logic and other fields, even among theorists who criticize aspects of it.<ref>{{multiref | {{harvnb|Brun|2003|p=19–22}} | {{harvnb|Peregrin|Svoboda|2016|p=55}} }}</ref> In some cases, individual logic translations are criticized based on the claim that they are unable to accurately represent all the aspects and nuances of the original text. For example, logical vocabulary is usually unable to capture things like [[sarcasm]], indirect [[insinuation]], or [[Prosodic stress|emphasis]]. In this regard, many aspects of the meaning of the original expression that go beyond truth value, validity, and logical structure are frequently ignored.<ref>{{harvnb|Magnus|Button|Thomas-Bolduc|Zach|2021|p=73-4, 259-60}}</ref> On the level of informal inferences, there are various expressions that cannot easily be represented using the precise but limited languages of formal logic.<ref>{{multiref | {{harvnb|Hintikka|2023}} | {{harvnb|Hurley|2018|p=263}} | {{harvnb|Brun|2003|p=19, 241}} }}</ref> For these reasons, it is sometimes controversial whether a specific logic translation is correct. When a logic translation is used to defend the conclusion of a natural language argument, one way to undermine such a defense is to claim that the logic translation is incorrect. This implies that insights gained from the formal logical analysis do not carry any weight for the original argument.<ref name="auto"/>

Another type of criticism is not directed at logic translations themselves but at how they are discussed in many standard works and courses of logic. In this regard, theorists like Georg Brun, Peregrin, and Svoboda argue that such works do not provide a proper discussion of the role and limitations of logic translations. Instead, it is claimed that they merely treat this topic as a side note. They may provide a few examples but their main focus is on the formal systems themselves. This way, there is no in-depth discussion of how these systems are applied to ordinary arguments.<ref>{{multiref | {{harvnb|Brun|2003|p=17, 19, 21, 195}} | {{harvnb|Peregrin|Svoboda|2013|p=2900}} | {{harvnb|Peregrin|Svoboda|2016|p=55}} }}</ref>

== See also ==
*[[Common Logic]]
*[[Double-negation translation]]
*[[Standard translation]]

== References ==
=== Notes ===
{{notelist}}

=== Citations ===
{{Reflist}}

=== Sources ===
{{refbegin|30em}}
*{{cite journal |last1=Baumgartner |first1=Michael |last2=Lampert |first2=Timm |title=Adequate formalization |journal=Synthese |date=September 2008 |volume=164 |issue=1 |pages=93–115 |doi=10.1007/s11229-007-9218-1 |s2cid=15396554 |url=https://boris.unibe.ch/117786/ |access-date=27 March 2023 |archive-date=15 April 2023 |archive-url=https://web.archive.org/web/20230415005452/https://boris.unibe.ch/117786/ |url-status=live }}
* {{cite book |last1=Blackburn |first1=Simon |title=A Dictionary of Philosophy |date=24 March 2016 |publisher=Oxford University Press |isbn=9780198735304 |url=https://www.oxfordreference.com/view/10.1093/oi/authority.20110803100432990 |language=en |chapter=rule of inference |access-date=8 January 2022 |archive-date=8 January 2022 |archive-url=https://web.archive.org/web/20220108194809/https://www.oxfordreference.com/view/10.1093/oi/authority.20110803100432990 |url-status=live |page=422 }}
* {{cite book |last1=Blackburn |first1=Simon |title=The Oxford Dictionary of Philosophy |date=1 January 2008 |publisher=Oxford University Press |isbn=978-0-19-954143-0 |url=https://www.oxfordreference.com/view/10.1093/oi/authority.20110803095423356 |language=en |chapter=argument |access-date=8 January 2022 |archive-date=8 January 2022 |archive-url=https://web.archive.org/web/20220108194756/https://www.oxfordreference.com/view/10.1093/oi/authority.20110803095423356 |url-status=live }}
* {{cite book |last1=Blackburn |first1=Simon |title=The Oxford Dictionary of Philosophy |date=1 January 2008a |publisher=Oxford University Press |isbn=978-0-19-954143-0 |url=https://www.oxfordreference.com/display/10.1093/oi/authority.20110803105953851;jsessionid=7B8D604DEBF650724327239FB7E268F8 |language=en |chapter=truth conditions |access-date=27 March 2023 |archive-date=27 March 2023 |archive-url=https://web.archive.org/web/20230327132658/https://www.oxfordreference.com/display/10.1093/oi/authority.20110803105953851;jsessionid=7B8D604DEBF650724327239FB7E268F8 |url-status=live }}
* {{cite journal |last1=Blair |first1=J. Anthony |last2=Johnson |first2=Ralph H. |title=Informal Logic: An Overview |journal=Informal Logic |year=2000 |volume=20 |issue=2 |doi=10.22329/il.v20i2.2262 |url=https://philpapers.org/rec/BLAILA-3 |access-date=29 December 2021 |archive-date=9 December 2021 |archive-url=https://web.archive.org/web/20211209195317/https://philpapers.org/rec/BLAILA-3 |url-status=live |pages=93–107 |doi-access=free }}
* {{cite book |last1=Borchert |first1=Donald |title=Macmillan Encyclopedia of Philosophy, 2nd Edition |date=2006 |publisher=Macmillan |url=https://philpapers.org/rec/BORMEO |chapter=Logic, Non-Classical |access-date=4 January 2022 |archive-date=12 January 2021 |archive-url=https://web.archive.org/web/20210112065913/https://philpapers.org/rec/BORMEO |url-status=live |isbn=978-0-02-865790-5 }}
*{{cite book |last1=Brun |first1=Georg |title=Die richtige Formel : Philosophische Probleme der logischen Formalisierung |date=2003 |publisher=Ontos Verlag |location=Frankfurt |language=de |isbn=3-937202-13-7 }}
* {{cite book |last1=Bunt |first1=H. |last2=Muskens |first2=Reinhard |last3=Thijsse |first3=E. |title=Computing Meaning: Volume 2 |date=6 December 2012 |publisher=Springer Science & Business Media |isbn=978-94-010-0572-2 |page=15 |language=en }}
* {{cite book |last1=Byrne |first1=Ruth M. J. |last2=Evans |first2=Jonathan St B. T. |last3=Newstead |first3=Stephen E. |title=Human Reasoning: The Psychology Of Deduction |date=18 June 2019 |publisher=Routledge |isbn=9781317716266 |page=59 |language=en }}
* {{cite journal |author-link=Robert Causey |last1=Causey |first1=Robert L. |title=Herbert R. Otto. The linguistic basis of logic translation. University Press of America, Washington, D. C., 1978, x + 201 pp. |journal=Journal of Symbolic Logic |date=June 1980 |volume=45 |issue=2 |pages=373–374 |doi=10.2307/2273204 |jstor=2273204 |s2cid=121994474 }}
* {{cite book |last1=Colman |first1=Andrew M. |title=A Dictionary of Psychology |date=1 January 2009 |publisher=Oxford University Press |isbn=978-0-19-953406-7 |url=https://www.oxfordreference.com/display/10.1093/oi/authority.20110803100112564;jsessionid=9E8800D02D072B638EDB50ADBDF15026 |language=en |chapter=logical analysis |access-date=27 March 2023 |archive-date=9 October 2023 |archive-url=https://web.archive.org/web/20231009131813/https://www.oxfordreference.com/display/10.1093/oi/authority.20110803100112564;jsessionid=9E8800D02D072B638EDB50ADBDF15026 |url-status=live }}
* {{cite book |last1=Craig |first1=Edward |title=Routledge Encyclopedia of Philosophy |date=1996 |publisher=Routledge |url=https://philpapers.org/rec/BEAREO |chapter=Formal and informal logic |access-date=29 December 2021 |archive-date=16 January 2021 |archive-url=https://web.archive.org/web/20210116111145/https://philpapers.org/rec/BEAREO |url-status=live |isbn=978-0-415-07310-3 }}
*{{cite book |last1=Dowden |first1=Bradley H. |title=Logical Reasoning |date=2020 |url=https://www.csus.edu/indiv/d/dowdenb/4/logical-reasoning-archives/Logical-Reasoning-2020-05-15.pdf |access-date=27 March 2023 |archive-date=2 June 2023 |archive-url=https://web.archive.org/web/20230602004345/https://www.csus.edu/indiv/d/dowdenb/4/logical-reasoning-archives/Logical-Reasoning-2020-05-15.pdf |url-status=live }} (for an earlier version, see: {{cite book |last1=Dowden |first1=Bradley Harris |title=Logical Reasoning |date=1993 |publisher=Wadsworth Publishing Company |isbn=9780534176884 |language=en |ref=none }})
* {{cite book |last1=Dyckhoff |first1=Roy |last2=Herre |first2=Heinrich |last3=Schroeder-Heister |first3=Peter |title=Extensions of Logic Programming: 5th International Workshop, ELP '96, Leipzig, Germany, March 28 - 30, 1996. Proceedings. |date=13 March 1996 |publisher=Springer Science & Business Media |isbn=978-3-540-60983-4 |pages=21, 31–2 |language=en }}
* {{cite book |last1=Engel |first1=S. Morris |title=With Good Reason an Introduction to Informal Fallacies |date=1982 |url=https://philpapers.org/rec/ENGWGR |chapter=2. The medium of language |access-date=2 January 2022 |archive-date=1 March 2022 |archive-url=https://web.archive.org/web/20220301065815/https://philpapers.org/rec/ENGWGR |url-status=live |isbn=978-0-312-08479-0 |pages=59–92 }}
* {{cite journal |last1=Franks |first1=Bridget A. |last2=Therriault |first2=David J. |last3=Buhr |first3=Miriam I. |last4=Chiang |first4=Evelyn S. |last5=Gonzalez |first5=Claire M. |last6=Kwon |first6=Heekyung K. |last7=Schelble |first7=Jenni L. |last8=Wang |first8=Xuesong |title=Looking back: reasoning and metacognition with narrative texts |journal=Metacognition and Learning |date=August 2013 |volume=8 |issue=2 |pages=146 |doi=10.1007/s11409-013-9099-2 |s2cid=255162310 }}
*{{cite book |last1=Fu |first1=Tzu-Keng |last2=Kutz |first2=Oliver |title=Proceedings of the Twenty-Fifth International Florida Artificial Intelligence Research Society Conference |isbn=978-1-57735-558-8 |chapter=The Analysis and Synthesis of Logic Translation |date=2012 |publisher=AAAI Press |location=Palo Alto, CA }}
* {{cite book |last1=Gabbay |first1=Dov M. |last2=Ohlbach |first2=Hans J. |title=Temporal Logic: First International Conference, ICTL '94, Bonn, Germany, July 11 - 14, 1994. Proceedings |date=29 June 1994 |publisher=Springer Science & Business Media |isbn=978-3-540-58241-0 |pages=462–3 |language=en }}
* {{cite book |last1=Garrett |first1=Brian |title=What is this Thing Called Metaphysics? |date=25 February 2011 |publisher=Taylor & Francis |isbn=978-1-136-79269-4 |page=28 |language=en }}
* {{cite web |last1=Garson |first1=James |title=Modal Logic: 13. Bisimulation |url=https://plato.stanford.edu/entries/logic-modal/#Bis |website=The Stanford Encyclopedia of Philosophy |publisher=Metaphysics Research Lab, Stanford University |access-date=22 February 2023 |date=2023 |archive-date=7 October 2020 |archive-url=https://web.archive.org/web/20201007121222/https://plato.stanford.edu/entries/logic-modal/#Bis |url-status=live }}
* {{cite book |last1=Gelbukh |first1=Alexander |title=Computational Linguistics and Intelligent Text Processing: 8th International Conference, CICLing 2007, Mexico City, Mexico, February 18-24, 2007, Proceedings |date=7 February 2007 |publisher=Springer Science & Business Media |isbn=978-3-540-70938-1 |language=en }}
* {{cite book |last1=Groat |first1=Linda N. |last2=Wang |first2=David |title=Architectural Research Methods |date=11 February 2002 |publisher=John Wiley & Sons |isbn=978-0-471-33365-4 |page=283 |language=en }}
* {{cite book |last1=Hansson |first1=Sven Ove |last2=Hendricks |first2=Vincent F. |title=Introduction to Formal Philosophy |date=24 October 2018 |publisher=Springer |isbn=978-3-319-77434-3 |page=61 |language=en }}
* {{cite web |last1=Hintikka |first1=Jaakko |title=Logical notation |url=https://www.britannica.com/topic/logic/Logical-notation |website=www.britannica.com |access-date=15 February 2023 |language=en |date=2023 }}
*{{cite book |last1=Hurley |first1=Patrick J. |title=A concise introduction to logic |date=2018 |publisher=Cengage Learning |location=Boston, MA |isbn=978-1-305-95809-8 |edition=Thirteenth }}
* {{cite book |last1=Jamieson |first1=D. |title=Language, Mind, and Art: Essays in Appreciation and Analysis, in Honor of Paul Ziff |date=9 March 2013 |publisher=Springer Science & Business Media |isbn=9789401583138 |page=34 |language=en }}
* {{cite web |last1=Janssen |first1=Theo M. V. |last2=Zimmermann |first2=Thomas Ede |title=Montague Semantics |url=https://plato.stanford.edu/entries/montague-semantics/#Int |website=The Stanford Encyclopedia of Philosophy |publisher=Metaphysics Research Lab, Stanford University |at=1. Introduction |date=2021 |access-date=27 March 2023 |archive-date=16 April 2021 |archive-url=https://web.archive.org/web/20210416105851/https://plato.stanford.edu/entries/montague-semantics/#Int |url-status=live }}
* {{cite journal |last1=Kuhn |first1=Tobias |title=A Survey and Classification of Controlled Natural Languages |journal=Computational Linguistics |date=March 2014 |volume=40 |issue=1 |page=152 |doi=10.1162/COLI_a_00168 |s2cid=14586568 |arxiv=1507.01701 }}
* {{cite book |last1=MacNish |first1=Craig |last2=Pearce |first2=David |last3=Pereira |first3=Luis M. |title=Logics in Artificial Intelligence: European Workshop JELIA '94, York, UK, September 5-8, 1994. Proceedings |date=10 August 1994 |publisher=Springer Science & Business Media |isbn=978-3-540-58332-5 |pages=366–7 |language=en }}
*{{cite book |title=forall x: Calgary: An Introduction to Formal Logic |first1=P. D. |last1=Magnus |first2=Tim |last2=Button |first3=Aaron |last3=Thomas-Bolduc |first4=Richard |last4=Zach |first5=J. Robert |last5=Loftis |first6=Robert |last6=Trueman |date=2021 |location=Calgary |publisher=University of Calgary |isbn=979-8527349504 |url=https://forallx.openlogicproject.org/forallxyyc.pdf |access-date=27 March 2023 |archive-date=16 February 2023 |archive-url=https://web.archive.org/web/20230216093131/https://forallx.openlogicproject.org/forallxyyc.pdf |url-status=live }}
* {{cite book |last1=Maher |first1=Michael |title=Logic Programming: Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming |date=1996 |publisher=MIT Press |isbn=978-0-262-63173-0 |page=65 |language=en }}
* {{cite web |last1=Moschovakis |first1=Joan |title=Intuitionistic Logic |url=https://plato.stanford.edu/entries/logic-intuitionistic/#RejeTertNonDatu |website=The Stanford Encyclopedia of Philosophy: 1. Rejection of Tertium Non Datur |publisher=Metaphysics Research Lab, Stanford University |access-date=11 March 2023 |date=2022 |archive-date=16 December 2022 |archive-url=https://web.archive.org/web/20221216154821/https://plato.stanford.edu/entries/logic-intuitionistic/#RejeTertNonDatu |url-status=live }}
*{{cite journal |last1=Mossakowski |first1=Till |last2=Diaconescu |first2=Răzvan |last3=Tarlecki |first3=Andrzej |title=What is a Logic Translation? |journal=Logica Universalis |date=July 2009 |volume=3 |issue=1 |pages=95–124 |doi=10.1007/s11787-009-0005-2 |s2cid=14296432 }}
* {{cite book |last1=Otto |first1=H. R. |last2=Tuedio |first2=J. |title=Perspectives on Mind |date=6 December 2012 |publisher=Springer Science & Business Media |isbn=978-94-009-4033-8 |page=315 |language=en }}
*{{cite book |last1=Pease |first1=Adam |last2=Li |first2=John |title=Theory and Applications of Ontology: Computer Applications |date=2010 |publisher=Springer Netherlands |isbn=978-90-481-8847-5 |pages=245–258 |url=https://link.springer.com/chapter/10.1007/978-90-481-8847-5_11 |language=en |chapter=Controlled English to Logic Translation |doi=10.1007/978-90-481-8847-5_11 |access-date=27 March 2023 |archive-date=17 February 2023 |archive-url=https://web.archive.org/web/20230217091216/https://link.springer.com/chapter/10.1007/978-90-481-8847-5_11 |url-status=live }}
*{{cite journal |last1=Peregrin |first1=Jaroslav |last2=Svoboda |first2=Vladimír |title=Criteria for logical formalization |journal=Synthese |date=September 2013 |volume=190 |issue=14 |pages=2897–2924 |doi=10.1007/s11229-012-0104-0 |s2cid=255069143 }}
*{{cite journal |last1=Peregrin |first1=Jaroslav |last2=Svoboda |first2=Vladimír |title=Logical Formalization and the Formation of Logic(s) |journal=Logique et Analyse |date=2016 |issue=233 |pages=55–80 |jstor=26767818 |url=https://www.jstor.org/stable/26767818 |issn=0024-5836 |access-date=27 March 2023 |archive-date=21 February 2023 |archive-url=https://web.archive.org/web/20230221084906/https://www.jstor.org/stable/26767818 |url-status=live }}
* {{cite book |last1=Quesada |first1=José F. |last2=Mateos |first2=Francisco-Jesús Martín |last3=Lopez-Soto |first3=Teresa |title=Future and Emergent Trends in Language Technology: First International Workshop, FETLT 2015, Seville, Spain, November 19-20, 2015, Revised Selected Papers |date=25 April 2016 |publisher=Springer |isbn=978-3-319-33500-1 |language=en }}
*{{cite thesis |last1=Rabe |first1=Florian |title=Representing Logics and Logic Translations |date=2008 |publisher=Jacobs University Bremen |location=Bremen |url=https://kwarc.info/people/frabe/Research/phdthesis.pdf |type=PhD dissertation }}
* {{cite journal |last1=Saule |first1=Burbekova |last2=Aisulu |first2=Nurzhanova |title=Problems of Translation Theory and Practice: Original and Translated Text Equivalence |journal=Procedia - Social and Behavioral Sciences |date=July 2014 |volume=136 |pages=122 |doi=10.1016/j.sbspro.2014.05.300 |doi-access=free }}
* {{cite book |last1=Shapiro |first1=Stewart |title=Varieties of Logic |date=4 September 2014 |publisher=OUP Oxford |isbn=978-0-19-102551-8 |page=75-6 |language=en }}
* {{cite book |last1=Stairs |first1=Allen |title=A Thinker's Guide to the Philosophy of Religion |date=29 September 2017 |publisher=Routledge |isbn=978-1-351-21981-5 |page=343 |language=en }}
* {{cite book |last1=Turetzky |first1=Philip |title=The Elements of Arguments: An Introduction to Critical Thinking and Logic |date=11 April 2019 |publisher=Broadview Press |isbn=978-1-4604-0646-5 |page=35 |language=en }}
* {{cite book |last1=Velleman |first1=Daniel J. |title=How to Prove It: A Structured Approach |date=16 January 2006 |publisher=Cambridge University Press |isbn=9780521675994 |page=8, 103 |language=en }}
* {{cite book |last1=Walton |first1=Douglas N. |title=Informal Fallacies: Towards a Theory of Argument Criticisms |date=1987 |publisher=John Benjamins |url=https://philpapers.org/rec/WALIFT |chapter=1. A new model of argument |access-date=2 January 2022 |archive-date=2 March 2022 |archive-url=https://web.archive.org/web/20220302001111/https://philpapers.org/rec/WALIFT |url-status=live |isbn=978-1-55619-010-0 |pages=1–32 }}
* {{cite book |last1=Yaqub |first1=Aladdin M. |title=An Introduction to Metalogic |date=24 October 2014 |publisher=Broadview Press |isbn=978-1-77048-381-1 |page=87 |language=en }}
* {{cite book |last1=Zoya |first1=Durdik |title=Architectural Design Decision Documentation through Reuse of Design Patterns |date=7 July 2016 |publisher=KIT Scientific Publishing |isbn=978-3-7315-0292-0 |page=77 |language=en }}
{{refend}}
{{Formal semantics}}
[[Category:Logic]]
[[Category:Semantics]]
[[Category:Translation]]