「語義解釋」(semantic interpretation)是形式語義學的一個重要概念，是指為自然語言句法單位(包括句子、分句、詞組、詞)所提供的能代表其語義的表達式，這個表達式一般包含個體詞和函數(亦稱謂詞)以及各種數學／邏輯符號，例如以下句子
的一個語義解釋便是以下表達式：
在上式中，j和 m是代表John和Mary的個體詞，LOVE是以兩個個體為論元的函數，其中第一和第二個論元分別對應loves的主語和賓語。不同的形式語義學流派採用不同的方法以得到語義解釋，某些方法在形式上跟「邏輯推理」非常相似。本文主旨是介紹在這方面有突出表現的兩個語法-語義學流派－「類型-邏輯語法」和「詞匯功能語法」。不過，在開始介紹上述流派前，須先簡介與「蘊涵式」和「函數」有關的一些基本知識。
「蘊涵式」是邏輯「公式」(formula)的一種，具有p→q的形式，其中「→」是代表「蘊涵」(implication)的符號，這個符號一般可譯成「如果...，則」，p和q則都是公式，它們分別是這個蘊涵式的「前件」(antecedent)和「後件」(consequent)。
接下來介紹兩條與蘊涵式有關的「推理規則」。第一條推理規則是「肯定前件」(modus ponens)，亦稱「→消去」(→ elimination)規則，簡稱「→E」，這條規則具有以下「自然演繹」(natural deduction)形式：
上圖中的橫線可以粗略地看成代表「推導」，即可以從橫線上的兩條公式(「前提」premise)推導出橫線下的公式(「結論」conclusion)，橫線右側的→E是這個推理的理據。上圖的直觀意思是，給定前提「如果p，則q」和p，便可以推導出結論q，這是有效的推理。請注意在這個推理中，前提中原有的→在結論中消失了，故稱「→消去」規則。
第二條推理規則是「假設推理」(hypothetical reasoning)，亦稱「→引入」(→ introduction)規則，簡稱「→I」，這條規則具有以下「自然演繹」形式：
上圖中被置於方括號內的p是推理的「假設」(hypothesis)，其右上角的數字n是假設的序號(一個推理可以包含多個假設，所以要用序號識別)。上圖中的橫向省略號代表推理中可能包括的其他假設或前提，縱向省略號則代表某個以q為中間結論的推導過程。最下一條橫線右側的→I, n是得到最終結論的理據，這裡的數字n代表前面引入序號為n的假設在這裡被「釋放」(discharged)了。請注意所有在推理中被引入的假設都必須逐一被釋放，為清晰標明當前被釋放的假設是哪一個假設，須在理據上標明被釋放假設的序號。上圖的直觀意思是，如在推理中引入假設p，並由此推出中間結論q，便可以推導出最終結論「如果p，則q」，這是有效的推理。請注意在這個推理中，最終結論包含中間結論所沒有的→，故稱「→引入」規則。
「函數」是當代形式語義學常用來表達語義的方式，它包含兩方面內容：類型和表達形式。一個函數的「類型」(type)可以寫成σ→τ的形式，其中「→」是代表「映射」(mapping，亦即「函數關係」)的符號，σ和τ則都是類型，它們分別是這個函數的「論元」(argument)和「值」(value)的類型。函數可以有多種表達形式，例如在數學上便採用f(x) = x2這種方式表達「二次方函數」。形式語義學則常常使用「λ表達式」，這種表達式具有λx[C(x)]的形式，其中x是代表論元的變項，C(x)則代表把這個函數作用於x後所得的值，例如上述「二次方函數」便可以表達成λx[x2]的形式。
看到這裡，有些讀者可能已發現，「蘊涵」的符號「→」同時又是「映射」的符號，而且蘊涵式p→q與函數類型σ→τ有相同的形式，這反映了「蘊涵」與「函數」之間存在對應關係。不僅如此，前面介紹的兩條推理規則也有相對應的λ表達式運算。第一種運算稱為「λ還原」(λ-reduction)，它是把函數作用於論元的運算。設有函數λx[C(x)]，現把它作用於論元a，會得到以下結果：λx[C(x)](a) = C(a)。由此可見，「λ還原」運算的結果是消去λ表達式中的λ算子，這跟「→E」規則的結果是消去→何其相似！從類型上看，如果某函數具有類型σ→τ，把這個函數作用於具有類型σ的東西，會得到具有類型τ的東西，這跟「→E」規則把p→q與p結合後得到q又何其相似！
λ還原的運算步驟很簡單，就是去掉λx[C(x)]中外層的λx[...]，並把a代入C(x)中的x，從而得到C(a)。不過，如果λ表達式包含多個λ符號，而a本身又是一個λ表達式，其運算可以頗為複雜，這時便要細心觀察，弄清楚哪一個是函數，哪一個是論元，以下用一個例子以說明這一點。設我們要把函數λAλx[A(x)]作用於論元λy[B(y)]，首先得到
| λAλx[A(x)](λy[B(y)]) | |
| = | λx[λy[B(y)](x)] |
可以看到上面最後一行λx[...]內的λy[B(y)]是函數，緊接其後的x則是論元，所以我們要繼續對λx[...]內的式子進行λ還原如下：
| λx[λy[B(y)](x)] | |
| = | λx[B(x)] |
上面最後一行就是最終的運算結果。
第二種運算稱為「λ抽象」(λ-abstraction)，它是推導出函數的運算。設有包含自由變項x的表達式C(x)，「自由變項」(free variable)是指邏輯公式中沒有受到任何量詞或者λ算子約束的變項。在此情況下，可以用λ算子約束x，即把這個表達式改寫成λx[C(x)]。由此可見，「λ抽象」運算的結果是把λ算子引入到一個表達式中，這跟「→I」規則的結果是引入→何其相似！舉例說，設有邏輯公式∀x∃z[P(x, y, z, w)]，在這個公式中，x和z分別受量詞∀和∃約束，是「受約變項」(bound variable)，而y和w則是「自由變項」。在此情況下，可以進行兩次λ抽象運算使變項y和w受到約束，從而得到以下不含自由變項的公式：
從類型上看，如果某個具有類型τ的表達式包含具有類型σ的自由變項，那麼運用「λ抽象」運算，可以約束這個自由變項，並得到具有類型σ→τ的函數，這跟在推理中，如有某個中間結論q是基於引入假設p而得，那麼運用「→I」規則，可以釋放這個假設，並得到蘊涵式p→q又何其相似！
至此我們看到，蘊涵與函數存在重重對應關係，此一對應關係在形式語義學界、邏輯學界和理論計算機學界稱為「柯里-霍華德對應」(Curry-Howard Correspondence)，現把此一對應關係總結成下表：
| 蘊涵關係 | 函數關係 |
|---|---|
正由於存在上述對應關係，我們可以同步進行邏輯推理和確定語義解釋的過程，這是以下兩節要介紹的內容。
「類型-邏輯語法」(Type-Logical Grammar，以下簡稱TLG)是「範疇語法」(Categorial Grammar)的多個支派之一(註1)，而範疇語法則是最多形式語義學者採用的語法體系。TLG的一個特點是把各類句法單位表達成類似邏輯公式的「範疇」(category)，它把名詞詞組、普通名詞(詞組)和句子的範疇定為基本範疇，分別用np、n和s代表(註2)，並把其他句法單位的範疇表達成這些基本範疇之間的蘊涵關係。舉例說，英語不及物動詞(詞組)的範疇是np\s，這裡的「\」代表「前件在左蘊涵」，「\」的左面和右面分別標示這個蘊涵關係的前件和後件，因此np\s可被看成這樣的蘊涵關係：若在其左面加上一個名詞詞組(即其主語)，會得到一個句子，這正是不及物動詞(詞組)的特徵。類似地，英語一般形容詞的範疇是n/n，這裡的「/」代表「前件在右蘊涵」，「/」的右面和左面分別標示這個蘊涵關係的前件和後件，因此n/n可被看成這樣的蘊涵關係：若在其右面加上一個普通名詞(詞組)，會得到另一個普通名詞詞組，這正是一般形容詞的特徵。
當然，自然語言中還有更複雜的範疇，例如英語及物動詞的範疇是(np\s)/np，這是因為及物動詞可被看成這樣的蘊涵關係：若在其右面加上一個名詞詞組(即其賓語)，會得到一個不及物動詞詞組。由於不及物動詞詞組本身也是蘊涵關係，及物動詞是一個「有向二重蘊涵關係」，因為它的後件是另一個蘊涵關係。學者之所以把及物動詞處理成有向二重蘊涵關係，是因為根據當代的英語句法分析，(1)這種英語及物句具有如以下「句法結構樹形圖」所示的句法結構，即及物動詞loves先與其右面的賓語名詞詞組Mary組成一個動詞詞組loves Mary，然後這個動詞詞組才與其左面的主語名詞詞組John組成句子：
TLG的另一特點是在句法與語義之間建立對應關係，此一對應關係體現為兩方面。第一，每一個句法「範疇」都有相對應的語義「類型」。TLG沿襲謂詞邏輯的做法，把「個體」和「真值」定為兩個基本類型，以下分別用e和t代表，分別作為名詞詞組和句子的類型，而普通名詞(詞組)的類型則是函數類型e → t，其他句法單位的類型也可以表示成相應的函數類型。舉例說，由於英語不及物動詞(詞組)的範疇是np\s，即分別以np和s為前件和後件的蘊涵關係，相應地不及物動詞(詞組)的類型是分別以e類型的東西和t類型的東西為論元和值的函數，即具有類型e → t的函數(註3)。類似地，由於一般形容詞和及物動詞的範疇分別是n/n和(np\s)/np，這兩種句法單位的類型相應為(e → t) → (e → t)和e → (e → t)。第二，每一個自然語言詞項都有相對應的個體詞(一般表現為單個小寫字母)或λ表達式以作為其語義解釋。正由於範疇與類型存在對應關係，而範疇又可被看成邏輯公式，根據前述的「柯里-霍華德對應」，使用範疇進行邏輯推理的過程同時就是確定語義解釋的過程。
至此我們看到，在TLG下，句法組合、邏輯推理和確定語義解釋這三個過程存在對應關係。有趣的是，上述三個過程可以同步進行。在具體操作上，TLG在「詞庫」(lexicon)中為每個詞項提供其語義解釋和範疇。把這些範疇當作邏輯公式，並把「\」和「/」符號當作蘊涵符號「→」處理，我們便可以利用前面介紹的兩條推理規則進行邏輯推理，並同時利用前面介紹的兩種λ表達式運算確定語義解釋，上述「句法-邏輯-語義同步推演」稱為「蘭貝克演算」(Lambek Calculus)(Winter (2016)也稱為「蘭貝克-范.本瑟姆演算」Lambek-van Benthem Calculus)。以下讓我們提供一些例子，設詞庫中有以下詞項：
| 詞項 | 語義解釋 : 範疇 |
|---|---|
首先考慮句子(1)，下圖展示就(1)進行蘭貝克演算的步驟：
在上圖中，我們首先寫出(1)所含的詞項，並從詞庫中取出這些詞項的語義解釋和範疇，這些範疇就是接下來推理的前提。接著從loves的範疇(np\s)/np和Mary的範疇np，根據→E規則推導出loves Mary的範疇np\s；與此同時，把loves的語義解釋作用於Mary的語義解釋並進行λ還原運算，便可得到loves Mary的語義解釋λx[LOVE(x, m)]。接著再從loves Mary的範疇np\s和John的範疇np，根據→E規則推導出John loves Mary的範疇s，此即句子的範疇；與此同時，把loves Mary的語義解釋作用於John的語義解釋並進行λ還原運算，便可得到John loves Mary的語義解釋LOVE(j, m)。請注意此一語義解釋正是(2)所示的命題。
接下來考慮以下「普通名詞 + 關係分句」結構：
在上例中，whom John loves是關係分句，而whom是這個關係分句中的關係詞。根據傳統語法學的觀點，whom起著雙重作用。第一，它連接著關係分句與其前的名詞(即上例中的girl)，並且標誌著關係分句是作為其前名詞的修飾語。第二，它充當關係分句中的賓語。可是，在當代句法學的觀點下，whom只起著上述第一個作用，其第二個作用改由一個空位來承擔(以下用△代表)。換句話說，(3)應被理解成girl whom John loves △，其中whom與△同指，所以採取賓格形式。下圖展示就(3)進行蘭貝克演算的步驟：
在上圖中，我們首先寫出(3)所含的詞項以及它們的語義解釋和範疇以作為推理的前提(其中△不是詞項，因此也不是前提)。由於John loves後缺少了賓語(即△所佔的位置)，我們無法進行推理，但可以在該位置加上變項w : np以作為假設(這個假設要放在方括號內且有序號1)。接著，運用兩次→E規則和進行兩次λ還原運算，可推導出John loves △的範疇s和語義解釋LOVE(j, w)。接著應用→I規則以釋放剛才加入的序號為1的假設，從而得到John loves的範疇s/np。請注意由於△位於John loves的右側，經釋放假設後所得的範疇應是s/np，即這樣的蘊涵關係：若在其右面加上一個名詞詞組，會得到一個句子。與此同時，對LOVE(j, w)進行λ抽象運算，便可把自由變項w約束起來，從而得到λw[LOVE(j, w)]。接著再運用兩次→E規則，便可推導出(3)的範疇n，即普通名詞的範疇。與此同時，進行兩次λ還原運算，便可得到(3)的語義解釋λu[GIRL(u) ∧ LOVE(j, u)]，意即既是女孩又為John所愛的個體，正是(3)的意思。
以上介紹的蘭貝克演算雖然展示了句法-邏輯-語義同步推演的優美之處，但它存在兩個缺點。首先，它只適用於英語這種有「句法結構定型性」(syntax configurationality)的語言，即有相對固定詞序和詞組結構(例如上面「句法結構樹形圖」所示的結構)的語言。正因為英語的一般及物句都具有如該圖所示的結構，我們才能把英語及物動詞的範疇確定為(np\s)/np。可是，世界上有一些語言，例如瓦爾皮里語(Warlpiri，澳大利亞的一種土著語言)，並無句法結構定型性，這些語言的及物動詞與其兩個論元的相對位置可以非常自由，而且也沒有證據顯示這些語言的及物動詞先與賓語組成動詞詞組，然後才與主語組成句子，因此無法把這些語言的及物動詞的範疇界定為類似(np\s)/np的形式。
其次，即使就英語而言，某些結構中的詞項的範疇也無法用「\」和「/」來界定。以前面討論過的關係分句為例，我們之所以能輕易處理該例子，純粹是因為在該例子中，△乃位於所在關係分句的邊緣。如果把該例子改為girl whom John met △ yesterday，我們便無法用「\」和「/」來界定John met yesterday的範疇，因為△並非位於這個結構的左／右側而是內部。事實上，為正確處理關係分句以及其他疑難現象，TLG採用新的用來代表範疇的符號，這些符號的共通點是不像「\」和「/」那樣有方向性。TLG的這種處理手法正揭示了蘭貝克演算的局限性。
「詞匯功能語法」(Lexical Functional Grammar，以下簡稱LFG)可被看成從「生成語法」(Generative Grammar)分裂出來的一個語法學流派(註4)，它的早期理論法幾乎只有語法方面的理論而沒有完整的語義理論。後來Dalrymple等人在早期理論的基礎上發展出「黏合語義學」(Glue Semantics)，可被看成當今形式語義學的一個流派(儘管處於較邊緣的地位)。LFG的特點是把自然語言的語法-語義現象表述成一系列平行但互有聯繫的「結構」，其中最重要的三個結構是「成分結構」(constituent structure，以下簡稱「c-結構」)、「功能結構」(functional structure，以下簡稱「f-結構」)和「語義結構」(semantic structure，以下簡稱「s-結構」)。c-結構大致相當於上面展示的「句法結構樹形圖」，這種結構會隨語言而異，例如上述樹形圖便只適用於英語，不適用於瓦爾皮里語。s-結構則大致相當於語義解釋，由於LFG的學者認為語義分析應具有普遍性，s-結構不應因語言而異。以上兩點的結果是，同一個意思的句法單位在不同語言中可能有不同的c-結構，但卻應有相同的s-結構，這就是LFG學者主張的「句法-語義不同構」(syntax/semantics non-isomorphism)原則。
可是，如何確保不同語言中有相同意思的句法單位有相同的s-結構(即使它們有不同的c-結構)？LFG的辦法是應用f-結構以作為c-結構與s-結構之間的中介。f-結構用來表示句子或名詞詞組的「語法功能」(grammatical function，例如主語、賓語、修飾語等)、「語法特徵」(grammatical feature，例如性、數、格、時、體等)等資訊，這些資訊一般被放置在一個「屬性-值矩陣」(attribute-value matrix)上。下圖展示句子(1)的f-結構(略去很多細節)：
在上圖中，A是句子(1)的f-結構的代號，這裡展示A的三個屬性PRED、SUBJ和OBJ。PRED屬性代表(1)的核心，其值'love<SUBJ,OBJ>'告訴我們(1)的核心是動詞love (略去其語法詞尾)，這個動詞帶有兩個論元，分別是其主語和賓語。SUBJ屬性和OBJ屬性分別代表(1)的主語和賓語，它們的值是另兩個f-結構。這兩個f-結構以B和C作為代號，其中B的PRED屬性及其值'John'告訴我們(1)的主語的核心是John，C的PRED屬性及其值'Mary'則告訴我們(1)的賓語的核心是Mary。請注意在上圖中，love、John和Mary這三個詞沒有先後次序，love也並非先與Mary結合然後才與John結合，因此上圖並非只適用於描述英語的情況。事實上，LFG學者認為主語、賓語等語法關係是適用於所有語言的概念，因此他們指出，句子(1)在不同語言中雖然可能表現為不同的c-結構，但卻應有相同的f-結構(以及s-結構)。
由於在LFG下，句法組合和確定語義解釋過程涉及c-結構、f-結構和s-結構這三者，此一過程體現為這三種結構之間的互動，以下簡介此一互動過程。此一過程的起點是詞庫，語法組合的最早階段就是從詞庫中取出詞項以構成c-結構。這些詞項帶有原始的句法和語義信息，接著便可以根據這些原始信息以及LFG的一套規則從c-結構推導出具體的f-結構，並同時把上述原始信息與具體的f-結構聯繫上，LFG把此一聯繫過程稱為「實例化」(instantiation)(註5)，經實例化的語義信息包含詞項的語義解釋和類似邏輯公式的「邏輯黏合式」(logical glue)。根據前述的「柯里-霍華德對應」，使用邏輯黏合式進行邏輯推理的過程與確定語義解釋的過程存在對應關係，而且這兩個過程可以同時進行。以下讓我們提供一些例子，首先再次考慮句子(1)，以下是句子(1)所含詞項經實例化的語義信息：
| 詞項 | 語義解釋 : 邏輯黏合式 |
|---|---|
在上表中，σ代表「s-結構」，Bσ代表代號為B的f-結構(亦即句子(1)中的主語John一詞的f-結構)的s-結構。上表中的「⊸」是「線性邏輯」中特有的蘊涵符號(有關線性邏輯與LFG的關係，請參閱下一節)，可被看成蘊涵符號「→」的變體，Cσ ⊸ (Bσ ⊸ Aσ)可被看成如下蕰涵關係：若得到Cσ和Bσ，便可得到Aσ (註6)。這反映了loves這個及物動詞的特性，因為loves若加上賓語(C)和主語(B)，便成為句子(A)。下圖展示利用上述語義信息就(1)進行「邏輯-語義同步推演」的過程(其關鍵在於把邏輯黏合式當作邏輯公式，並把「⊸」符號當作蘊涵符號「→」處理，)：
上圖中最後一行的邏輯黏合式是Aσ，由於A是(1)的f-結構，這顯示上圖中最後一行的LOVE(j, m)就是(1)的語義解釋。
上圖顯示LFG就(1)進行的推演跟TLG的推演非常相似，但兩者其實存在一些重要差異。首先，TLG的推演是邏輯-句法-語義三者同步進行推演，TLG的「\」和「/」符號既有句法意義(反映詞序)又有邏輯意義(代表「蘊涵」)；而LFG的推演則只是邏輯-語義兩者同步進行推演，LFG的「⊸」符號只有邏輯意義(代表「蘊涵」)而沒有句法意義。其次，TLG的「\」和「/」符號規定了函數和論元的相對位置，而LFG的「⊸」符號則沒有這種規定，因此在上圖中，即使把loves與Mary這兩個詞對調位置，仍然可以推演出上圖所示的最終結果。請注意由於LFG主張「句法-語義不同構」，上圖中的推演不必反映句子(1)的詞序，因此可以把loves與Mary對調位置。第三，在TLG下，及物動詞的語義解釋和範疇嚴格規定了這個詞必須先與賓語名詞(詞組)結合然後才與主語名詞(詞組)結合。在LFG下，及物動詞的語義解釋和邏輯黏合式雖然也反映結合的先後次序，但這種先後次序是可以改變的，即一個詞項可以有多於一個語義解釋和邏輯黏合式。舉例說，上表中loves的邏輯黏合式是Cσ ⊸ (Bσ ⊸ Aσ)，現在我們通過以下推演把它轉變為Bσ ⊸ (Cσ ⊸ Aσ)：
在以上推演中，我們先後引入兩個序號為1和2的假設，並進行兩次→E，接著又進行兩次→I，先後釋放假設1和假設2，從而得到loves的另一語義解釋和邏輯黏合式。讀者可自行驗證，利用這個新的語義解釋和邏輯黏合式進行邏輯-語義同步推演，可得到與前面相同的結果。
接下來再次考慮(3)所示的「普通名詞 + 關係分句」結構。為簡單起見，現假設已確定(3)的c-結構和f-結構，並得到(3)所含詞項經實例化的語義信息如下(註7)：
| 詞項 | 語義解釋 : 邏輯黏合式 |
|---|---|
請注意在上表中，我們使用前述loves的另一語義解釋和邏輯黏合式。另請注意由於girl只是普通名詞而非名詞詞組，它沒有自己的f-結構，但由於girl的語義解釋λx[GIRL(x)]是具有類型e→t的函數，上表把girl的邏輯黏合式寫成v ⊸ r的形式，其中v、⊸和r分別對應著e、→和t。下圖展示利用上述語義信息就(3)進行邏輯-語義同步推演的過程：
上圖顯示LFG就(3)進行的推演比TLG的推演簡單，上圖無需引入空位和相關的假設，也無需應用→I規則，這是因為在上圖中loves的邏輯黏合式是Bσ ⊸ (Cσ ⊸ Aσ)，正可與John的邏輯黏合式Bσ配合。換句話說，在LFG的推演中，loves可以先與主語John結合。反之，在TLG下，loves必須先與賓語名詞詞組結合，但在(3)中loves的賓語卻是一個空位，所以TLG的推導不能像LFG那樣簡單。以上例子顯示，由於LFG採取句法-語義不同構原則，在進行邏輯-語義同步推演時，無需理會詞序，也無需硬性規定及物動詞須先與賓語名詞詞組結合，因此LFG的推演較TLG的推演有較多的彈性。
形式語義學是使用邏輯學工具(以及數學工具)以研究語義問題的學科，當然會把邏輯學各分支的內容應用於研究中。不過，若單從「邏輯-語義同步推演」這一方面看，形式語義學對邏輯學的應用卻是有選擇性的。根據Barker (2003)和Asudeh (2023)，邏輯-語義同步推演所採用的邏輯系統不是一般經典邏輯(指命題邏輯和謂詞邏輯)而是「直覺主義邏輯」(Intuitionistic Logic)的某些子類。直覺主義邏輯有別於經典邏輯之處在於它排除經典邏輯的「排中律」(Law of the Excluded Middle)，因而不接受「反證法」(proof by contradiction)，即透過證明¬p會引致矛盾來間接證明p。事實上，形式語義學從不使用反證法進行邏輯-語義同步推演(註8)。除了排中律外，以下三條「結構規則」(structural rule)也是形式語義學流派排除的對象。第一條結構規則是「弱化」(Weakening)，這條規則具有以下「相繼式演算」(sequent calculus)形式：
在上圖中，(p1, ... pn)代表前提序列(可以是空序列)，⊢代表「可推導出」，上述規則的直觀意思是，把任意命題q加入到前提序列中的任何位置，可以推導出原來前提序列所能推導出的結論。第二條結構規則是「緊縮」(Contraction)，這條規則具有以下「相繼式演算」形式：
上述規則的直觀意思是，把前提序列中重複出現的前提q刪減一個，仍能推導出原來前提序列所能推導出的結論。第三條結構規則是「交換」(Commutativity)，這條規則具有以下「相繼式演算」形式：
上述規則的直觀意思是，把前提序列中任意兩個前提q和r對調位置，仍能推導出原來前提序列所能推導出的結論。請注意上述三條規則在經典命題邏輯下都是有效推理。
在直覺主義邏輯的框架下，如果排除上述三條結構規則的任意一條，便會得到「亞結構邏輯」(Substructural Logic)，因此亞結構邏輯是直覺主義邏輯的子類。在上述三條結構規則中，如果排除了「弱化」和「緊縮」，所得邏輯系統被稱為「資源敏感」(resource sensitive)的邏輯系統。在這種邏輯系統下，前提可被看成資源，而某前提被用來推導出結論可被看成該項資源在推導過程中被消耗掉。資源敏感的邏輯系統的特點就是要求每件資源(出現n次的同一個資源應被視為n件資源)都應被消耗掉，不容許出現不被消耗掉的多餘資源(所以要排除「弱化」規則)，也不容許刪除任何可被消耗掉的資源(所以要排除「緊縮」規則)。根據Klein & Sag (1985)，形式語義學名篇Montague (1973)上的邏輯-語義同步推演系統具有資源敏感性，後來其他形式語義學流派也都把資源敏感的邏輯系統應用於其邏輯-語義同步推演中。
接著讓我們看如不排除上述兩條結構規則，邏輯-語義同步推演會出現甚麼奇怪結果。首先，若容許「弱化」規則，就意味著某些包含多餘詞項的不合語法句子，也能被當作合語法的句子處理。以句子(1)為例，前面已顯示在TLG和LFG下，邏輯-語義同步推演可以為這句確定正確的語義解釋：LOVE(j, m)，我們可以把此一事實記作下式：
現在若應用上面展示的「弱化規則」，那麼*John loves Mary she這個包含多餘詞項的句子也能得到相同的語義解釋如下：
其次，自然語言的句子常有重複出現的詞項，這些詞項的每個單獨出現(occurrence)都在邏輯-語義同步推演過程中有其獨立貢獻，不能隨意刪掉。若容許「緊縮」規則，將意味著某些殘缺不全的不合語法句子也能被當作合語法的句子處理。舉例說，以下提供句子John loves Mary and Mary loves John的推演結果：
現在若應用上面展示的「緊縮規則」，那麼*John loves Mary and這個殘缺不全的句子也能得到相同的語義解釋如下：
在資源敏感的邏輯系統下，如果進一步排除「交換」規則，所得邏輯系統就是「蘭貝克邏輯」(Lambek Logic)，否則就是「線性邏輯」(Linear Logic)，這兩種邏輯分別正是TLG的蘭貝克演算和LFG的黏合語義學的邏輯基礎。排除「交換」規則意味著前提的位置有重要意義，不能隨意調動，這正是英語這種有相對固定詞序語言的特點。正因此一特點，蘭貝克演算適合用來對英語這類語言進行「句法-邏輯-語義同步推演」。可是，如前所述，並非所有語言都像英語那樣，有些語言有自由的詞序，因此蘭貝克邏輯並不適用於所有語言。事實上，為正確處理英語的關係分句以及其他疑難現象，TLG也不得不引入沒有方向性(即不受詞序影響)的符號，這其實局部偏離了蘭貝克邏輯。LFG則索性棄用蘭貝克邏輯而採用保留「交換」規則的線性邏輯，因此LFG的推演不用兼顧詞序。由於詞序是某些語言(如英語)的重要句法特徵，這意味著LFG的推演只能是「邏輯-語義同步推演」而不是「句法-邏輯-語義同步推演」。
除了蘭貝克邏輯和線性邏輯外，還有其他亞結構邏輯。在直覺主義邏輯的框架下，若只排除「弱化規則」，可得到「相干邏輯」(Relevance Logic)；若只排除「緊縮規則」，可得到「仿射邏輯」(Affine Logic)。由於這兩種邏輯沒有資源敏感性，它們並不應用於邏輯-語義同步推演中。作為總結，現把經典邏輯、直覺主義邏輯以及各種亞結構邏輯的相互關係表示成下圖(引自Asudeh (2023)，經刪略)：
