999精品在线视频,手机成人午夜在线视频,久久不卡国产精品无码,中日无码在线观看,成人av手机在线观看,日韩精品亚洲一区中文字幕,亚洲av无码人妻,四虎国产在线观看 ?

基于Lukasiewicz計算模型的六值命題邏輯公理體系構建*

2015-03-19 11:37:18林加華
楚雄師范學院學報 2015年6期
關鍵詞:語義系統

林加華,姜 華

(楚雄師范學院信息學院,云南 楚雄 675000)

基于Lukasiewicz計算模型的六值命題邏輯公理體系構建*

雖然經典命題邏輯在理論上已經趨于成熟,它既是可靠的又是完備的,但在現實世界中并不是每個命題均可直接用真與假來判斷。很顯然,對未來事件進行判斷的命題既不真也不假。為了改進經典命題邏輯的這種不足,本文在深入研究經典命題邏輯的基礎上,以Lukasiewicz計算模型為基礎,通過擴展經典命題邏輯的邏輯真值集,并采用擴展后的邏輯真值構成的賦值格對命題進行賦值。由此本文提出六值命題邏輯系統,記為£s。系統中否定了經典命題邏輯中的排中律,增加了對命題判斷的多樣性,增強了它對現實世界的表達能力。

經典命題邏輯;Lukasiewicz計算模型;六值命題邏輯

1.引言

由于人們對一個命題“非真即假,非假即真”判定的懷疑,這種懷疑是多值邏輯出現的內因。有著多值邏輯學之父稱號的著名邏輯學家Lukasiewicz提出除了邏輯真與邏輯假之外,還應該存在第三個邏輯真值I,I表示不確定的中間狀態。[1]事實上,這里中間狀態所表達的內涵是對未來事件發生與否的概率判斷。時間稍晚一些又有前蘇聯數學家Bochvar為了處理語義悖論提出了他自己的三值邏輯系統B3、由邏輯學家Kleene提出的三值邏輯系統K3、Godel提出的三值邏輯系統G3、由另外一個多值邏輯創始人Post提出的三值邏輯P3等等。他們大多數都在自己的三值邏輯的基礎上完成了更多值乃至n值邏輯系統的理論研究,取得了數理邏輯學領域的輝煌成就。

目前,對多值邏輯體系構建的研究主要存在兩條路徑。其一,以二值邏輯為基礎,擴展其邏輯真值集,借用某多值邏輯系統的計算推理模型,并提出自己的語義賦值及語義解釋,最后完成可靠性和完備性證明;其二,把研究重點放在計算模型的設計上,特別是對蘊涵算子的設計,等計算模型設計完成后,再尋找其語義賦值和語義解釋。[2]前者所構建的系統一般都能對可靠性和完備性進行證明并存在合理的語義賦值與語義解釋,但形式推理過程對原系統有依賴。后者,可謂全新開發,其突出的問題是難以進行語義賦值和語義解釋且完備性證明困難,甚至不存在完備性。本文的研究思路采用前者。

2.六值命題邏輯£s的語法構成

2.1命題符號與聯結詞

2.1.1 £s的組成符號

第一類包括可數無窮多個命題符號:A,B,C,…Z;a,b,c,…z以及由字母組合而成的有意義的字符串。第二類包括四個聯結詞:┐,∧,∨,→ 。第三類包括兩個技術性標點符號:( , )。它們依次被稱為左括號和右括號。由第一類符號、第二類符號和第三類符號組成的有窮序列稱之為邏輯符號,簡稱符號。由全體符號形成的集合稱為表達式,記為:Exp(£s)。

2.1.2 £s的聯結詞

邏輯聯結詞是構建任何邏輯系統的基石,同時也是不同邏輯系統之間的區別之一。本系統£s的邏輯聯結詞定義如下:

定義2.1(聯結詞):

(1) 否定聯結詞┐:┐A=1-A;

(2) 蘊涵聯結詞→:A→B=(1-A+B)∧1。

由(┐,→)可引出以下邏輯聯結詞的定義:

(3) 析取聯結詞∨:A∨B=(A→B)→B;

(4) 合取聯結詞∧:A∧B=┐(┐A∨┐B)。

很容易看出,£s的聯結詞的定義與經典命題邏輯的聯結詞定義已經有了很大的不同。正如上文所描述,它與盧氏多值邏輯系統中對聯結詞的定義相同[3]。本系統只是引用了它的定義形式,即盧氏多值邏輯的計算模型。但在真正的語義計算時,£s要遵循六值命題邏輯系統中關于語義的約束,所以不是簡單地去借用其計算模型,而是一種對它改進了的,在賦值格序圖偏序集上的應用。

2.2 六值命題邏輯£s的公式

2.2.1 £s公式的生成規則

六值命題邏輯£s的原子公式集和公式集分別記作Atom(£s)和Form(£s)。*表示三個聯結符號∧,∨和→中的任意一個。

定義2.2(Atom(£s))六值命題邏輯£s的一個表達式是Atom(£s)一個元,當且僅當它是一個單獨命題符號,即第一類符號。

定義2.3Form(£s) 設pForm(£s),當且僅當它能有限次使用以下的(1)~(3)規則生成:

(1)Atom(£s)Form(£s);

(2) 若pForm(£s),則┐pForm(£s);

(3) 若p,qForm(£s),則(p*q)Form(£s)。

定義2.3中的(1)、(2)和(3)是六值命題邏輯£s公式的形成規則。在公式的形成過程中特別強調是有限次地使用這三個規則,如果不能在有限次使用規則內形成則不是六值命題邏輯£s的公式。

2.2.2公式集相關說明

假設p,q是六值命題邏輯系統中的公式,則

(1)p中的聯結詞┐,∧,∨,→出現的總次數稱為公式p的復雜度。

(2)如果p作為q的一個部分出現,則稱p是q的子公式;如果p是q的子公式且p不等于q,則稱p是q的真子公式。

(3) 稱只出現在p中而不出現在p的任何真子公式中的那個聯結詞為p的主聯結詞;稱主聯結詞是否定聯結詞┐的公式為否定式;主聯結詞是合取聯結詞∧的公式為合取式;主聯結詞是析取聯結詞∨的公式為析取式;主聯結詞是蘊涵聯結詞→的公式為蘊涵式。

3.六值命題邏輯£s形式推演

3.1£s形式可推演性

定義3.1 (∑├A) ∑├A(A是由可形式推演或形式可證明的),當且僅當存在序列

A1,A2,…An,使得An=A,并且每一個Ak(1≤k≤n) 滿足以下條件之一:

(1)Ak是六值邏輯的公理,

(2)Ak∑,

(3)有i,j

如果存在一個由∑到A的推演,則稱A在£s系統中是由∑形式可推演的[4],記為∑├£sA,簡記為∑├A。否則,稱A在£s系統中不是由∑形式可推演的,記為∑├/ £sA,簡記為∑├/A。

3.2 六值命題邏輯£s形式推演規則

£s的形式推演規則與經典命題邏輯的形式推演規則在結構上相似,但卻也存在很多不同之處。主要區別在于:第一,經典命題邏輯系統支持排中律。第二,本系統擴展了邏輯真值集且采用了盧氏計算模型,所以,實際的形式推演過程與經典邏輯截然不同[5]。具體的推演規則如下:

設∑={A1,A2…Am},m為正整數,Am為£s的公式,有時為了推理方便也可以把∑寫成A1,A2,A3…的形式。另外,元素之間的次序關系是不重要的,且規定∑,A=∑A。

①自反規則(Ref) ②增加前提(+)

A├A如果∑├A,則∑,∑'├A。

③蘊涵消去規則(→-)(該規則也稱之為三段論,HS規則)

如果∑├A→B,∑├A,則∑├B。

④蘊涵引入規則(→+)(也稱為演繹規則)

如果∑,A├B,則∑├A→B。

⑤包含律(∈)

(i)如果A∑,那么∑├A。 (ii) 如果A∑并且∑Δ,那么Δ├A。

⑥分配律

(i)如果∑├A∧B,則(∑├A)∧(∑├B)。

(ii)如果∑├A∨B,則(∑├A)∨(∑├B)。

⑦結合律

(i)如果(∑├A)∧(∑├B),則∑├A∧B。

(ii)如果(∑├A)∨(∑├B),則∑├A∨B。

⑧雙重否定規則

A=┐┐A。

⑨德摩爾根定律

(i)(A∧B)=(A∨B)。 (ii)┐(A∨B)=(┐A∧┐B)。

3.3 六值命題邏輯£s的定理

若∑={A1,A2…Am}并∑├A可記為A1,A2…Am├A;若{∑∪A}├B可記為∑,A├B;若∑為空集,∑├A可記為├A。滿足以上三種情形之一時,稱A是可由六值邏輯系統推出的一個定理,簡稱A是£s定理。

上面的定理定義可描述為,凡是可從已知的前提公式或推理規則本身出發,通過有限次地應用推理規則而得到的結論都是£s定理, 一個形式可證明的公式是£s系統中的一個定理。

定理3.1(代入定理) 在永真式中,用一個或幾個命題形式代入到它的相應命題變元,并遵循:

(1)同名的命題形式只能代入同名的命題變元;

(2)這種代入必須處處進行,即一個代入命題形式必須取代所有同名的命題變元[6]。

那么代入結果仍然是命題形式,稱為永真式的代入示例,簡稱代入示例。如:A→(B→A),是六值命題邏輯的一條公理,它是永真式?,F在用“C→A”代入到所有變元“A”處,得(C→A)→(B→(C→A))也是永真式。代入定理可以成為形式推演的輔助性工具,但有一點必須強調:代入定理一定是從永真式開始進行代入的,否則不能保證代入結果的可靠性?!阺形式推演出的方法可表述為:從作為起始狀態的已知前提公式集出發,根據推理規則在公理代入定理的輔助下向目標狀態的轉化過程。

4.六值命題邏輯£s的真值體系

4.1 £s系統的賦值格

本文提出的£s有6個邏輯真值,即是“真”,“可能真”,“不可能假”,“不可能真”,“可能假”,“假”。分別對應的字母表示形式是“t”,“tp”,“┐fp”,“┐tp”,“fp”,“f”。規定“tp”和“fp”的邏輯值大于0.5,而“tp”和“fp”的邏輯值小于0.5。為了使表達更為嚴謹且使后文表述更為方便,現在集合的形式來規范它們。設集合D={“t”,“tp”,“┐fp”,“┐tp”,“fp”,“f”},Dt={“t”,“tp”,“┐fp”},Df={“┐tp”,“fp”,“f”},顯然集合Dt和Df都是集合D的子集,即Dt?D,Df?D。稱集合D為六值命題邏輯的邏輯真值集,稱子集Dt為六值命題邏輯的邏輯真值集的“近真子集”,稱子集Df為六值命題邏輯的邏輯真值的“近假子集”。為了直觀地描述其在邏輯上的大小關系,現為£s定義其賦值格序圖,見圖4.1。圖4.1 賦值格序圖

不難發現,在格序圖中有兩對不可比較的值。它們分別是tp和┐fp,fp和┐tp。因為不可比較,所以就不能直接參與運算。需要進行特殊的處理,規定如下:

(1)tp∧┐fp∈Dt,fp∧┐tp∈Df

(2)tp∨┐fp∈Dt,fp∨┐tp∈Df

(3)tp→┐fp∈Dt,fp→┐tp∈Df

需要要說明的是,tp,┐fp,fp和┐tp都不是公式,只是用來表示對公式的賦值。事實上,這所謂的特殊規定也完全符合人們的思維方式的。比如:

A:明天會下雨,可能是真的,即Aυ=tp。

B:明天會下雨,不可能是假的,即Bυ=┐fp。

A∧B表達的含義是相信A命題與B命題中可能性更小的那個。雖然A與B不可比較,但不管相信哪個,“明天會下雨”這件事基本上就是真的了。所以說A與B合取后就“近真”了。A∨B所表達的含義是相信A命題與B命題中可能性更大的那個。雖然A與B不可比較,但不管相信哪個,“明天要下雨”這件事基本上就是真的了,所以說也就“近真”了。fp和┐tp在∧與∨情形下同理。

4.2六值命題邏輯£s的語義約束

本系統是從經典命題邏輯擴展過來的,擴展的邏輯真值有:tp,┐fp, ┐tp,fp共4個,要想使已經擴展了的邏輯真值也有合理的語義解釋,就必須對它們做出合理的語義約束。在其它多值邏輯系統中也稱之為語義約束公理。然后證明它們在邏輯系統中語義解釋是無矛盾的,即任何一個表達式不會因為采用了不同的加減變換及等量替換而到不同的結果。下面就對本系統中所作的語義約束進行詳細的討論。

(1)互補約束

t-tp=┐tpt-┐tp=tptp+┐tp=t

t-┐fp=fpt-fp=┐fp┐fp+fp=t

t-f=tt-t=ft+f=t

這是一組最基本性質,是由否定聯結詞和邏輯真值格序圖共同決定的,其中“t”也可以解釋為語義中的“1”,即本系統中的“真”。如果有一個命題的語義賦值是“t”的話,那么對它的語義解釋就是真,是不容置疑的。例如:命題p:明天會下雨,當pυ=t時,那么就是說:明天是絕對會下雨的,雖然這個命題可能并不能與客觀實際相符(可能在客觀實際中沒有一種技術可以預報明天會絕對下雨),但是,一旦如果對它進行了賦值“真”,也就是“t”的話,那么在本系統推理中它就被認為是真的,是不容置疑的。換句說,如果懷疑已經被語義賦值為“真”的命題的真假,這本身就犯了邏輯錯誤。從另一個方面說,實際上,邏輯推理是考察命題與命題之間是否有邏輯關系,即前提命題與結論命題之間的關系,而不涉及命題本身所代表的含義。如:

p:牛會飛。

q:如果牛會飛,那么馬就不會吃草。

如果現在對p,q的語義賦值是pυ=t,qυ=t的話,那么就經過簡單的推理得出“馬不會吃草”。這個推理看似不合理,但實際上確有它的邏輯上的道理所在。這也正是數理邏輯推理中所謂的只考察命題與命題之間的邏輯關系,而不考察命題本身所代表的內容。

(2)同值加約束

tp+tp=tp

┐tp+┐tp=┐tp

fp+fp=fp

┐fp+┐fp=┐fp

這一組語義約束公理可能會有些費解,問題就在于在前文中所描述的語義推理是采用盧氏的計算模型,而盧氏的計算模型是在[0,1]上的精確的小數計算。例如:A→B=(1-A+B)∧1,如果對Aυ=0.7,Bυ=0.6,那么(A→B)υ=0.9。很顯然,它是數值的精確計算。本文提出的六值命題系統,從經典命題邏輯擴展而來,因此具有經典命題邏輯系統中的部分推理性質。這一組語義約束公理所要表達的內涵是:“可能真”加上“可能真”還是“可能真”,而“可能假”加上“可能假”還是“可能假”。舉例:張三說明天可能會下雨,李四也說明天可能會下雨,在旁邊聽了這兩個人的斷言的人,只能得到明天可能會下雨的信息,而不會是因為兩個人所說的“可能真”就累加起來變成明天一定會下雨。在一次推理中,一個可能真與兩個可能真,甚至成百上千個可能真累加,其結果在邏輯上是一樣的。

(3)*'+*'' =*'∨*'' ,其中 *',*'' {“tp”,“┐fp”,“┐tp”,“fp” }

注:∨表示在二者之中取大值。

這是一條很強的語義約束公理。實際上,它包含語義約束公理(2)。不僅如此,它包含的具體語義約束是比較多的,這里不一一列出了。但應特別注意的是*'和*''都不能是邏輯真值t。正如前文已經給出的,本系統的邏輯真值格序圖中存在兩對不可比較的邏輯真值。所以現在把它分成兩類情況來討論:

第一類:可比較加約束 第二類: 不可比較加約束

tp+┐tp=tp∨┐tp=tptp+┐fp=tp∨┐fp

tp+fp=tp∨fp=tp┐tp+fp=┐tp∨fp

┐fp+fp=┐fp∨fp=┐fp

┐fp+┐tp=┐fp∨┐tp=┐fp

第一類可比較的情形沒有完全列舉,如若需要知道其它沒有列舉出來的情況,只需按與第一類相同規則計算一下便知。在引入6個邏輯真值的時候已經規定了tp>0.5, ┐tp<0.5,所以tp與┐tp就是可比較的了,這一點在格序圖中也有所反應。所以可知,對tp與┐tp取大運算時得tp。正如:“tp+┐tp=tp∨┐tp=tp”。

第二類情形是對不可比較的兩對邏輯真值進行加運算的語義約束,是本系統中語義約束的精華之一。成功地解決了不可比較的邏輯真值之間運算的表達問題。關于它們之間相減的情況在下一個語義約束公理中給出。

(4) 不可比較減約束

*'- *''=*'∧*'' ,其中 *',* '' {“┐tp”,“fp” }

注:∧表示在二者之中取小值,* '與*''不取相同值。

由(4)直接展開的語義約束有:

┐tp-fp=┐tp∧fp

fp-┐tp=┐tp∧fp

關于另外一對不可比較的邏輯真值tp與┐fp之間的相減可以進行如下轉換:

tp-┐fp=tp-┐fp+1- 1=(1-┐fp)-(1-tp)=fp-┐tp=┐tp∧fp

┐fp-tp=┐fp-tp+1- 1=(1-tp) -(1-┐fp)=┐tp-fp=┐tp∧fp

(5)可比較減約束

tp-┐tp=tp

tp-fp=tp∧┐fp

┐fp-fp=┐fp

┐fp-┐tp=tp∧┐fp

語義約束公理(4),(5)似乎已經失去邏輯直觀主義者所說的“邏輯直觀”了,特別是語義約束公理(5),實際上它是可以通過上面的具有“邏輯直觀”的語義約束公理推導所得的。

例如:tp-┐tp=tp(演算過程如下)

tp→┐tp=(1-tp+┐tp)∧1

=(┐tp+┐tp)∧1

=┐tp∧1 (由于┐tp+┐tp=┐tp)

=┐tp

(6)取最短表達式約束

在涉及到不可比較的邏輯真值的蘊涵推理時,如果采用不同的運算方式得到多種長短不一的結果表達式取其最短的作為最終運算結果,例如:采用不同的運算方式得到了┐tp與┐tp∨fp,最終結果取┐tp。

4.3六值命題邏輯£s系統的語義解釋

上面已經給出了£s語法的形式表述,然而作為一種形式語言,就必須要給予它在特定邏輯真值集下的全方位解釋。包括其中的各類符號涵義,以及由這些符號所構成的各種公式所表示的事物的涵義。下面先作直觀的說明:

否定符號“┐”表示某事物發生的可能性的反面。析取符號“∨”表示取極大。即兩者運算取其大者。合取符號“∧”表示取極小,即兩者運算取其小者。這里“取其大者”與“取其小者”均是指在本系統提出的語義約束公理范疇下的“取其大值”與“取其小值”。在£s中已經沒有傳統意義上的“與”,“或”運算,取而代之的是“取大”,“取小”運算[7]。這也是多值邏輯與經典命題邏輯的區別之一。蘊涵符號“→”表示的是一種與盧氏三角模運算相伴隨的正則蘊涵算子,具體的運算法則是:A→B=(1-A+B)∧1。

對公式的語義解釋則根據£s系統對聯結詞定義和形式推規則進行的,另外關于6個邏輯真值的取值只要滿足格序圖即可,其本質是數值計算,這就為形式推演在計算機中通過編程的方式現實奠定了基礎。也是眾多數理邏輯研究人員選擇依據盧氏計算模型進行構建多值邏輯系統或以改造盧氏計算模型作為研究切入點的普遍原因。最后需要對一個普遍性原則進行說明:一般來說,在眾多不同的多值邏輯系統中,它們的“否定”,“合取”,“析取”,“等值”的含義是相同的,而唯一不同的是“蘊涵算子”。本文提出£s系統的構建也采用了該原則。

5.小結

本文是在經典命題邏輯的基礎上對其邏輯真值集進行了擴展,從原來只有真、假二值擴展到了擁有6個邏輯真值的多值邏輯,豐富了系統的表達能力。與其它多值邏輯系統有明顯不同的在于蘊涵式,其形式表達為A→B=(1-A+B)∧1。該式引用自盧氏正則蘊涵算子,本文重點研究對該蘊涵式進行的語義約束。原盧氏系統是在[0,1]區間上的無窮值邏輯系統,而本系統把無限邏輯值轉變成6個小區間,是對原盧氏系統的一種改進。誠然,本系統尚存在許多不足之處需要在后續工作將它不斷地完善,未來進一步的工作主要是要把多值邏輯與模糊邏輯相結合,在六值命題邏輯中加入模糊推理規則并在計算機中編程實現機器推理。

[1]羅玉忠.多值邏輯的形成探析[J].中山大學研究生學刊,1999,20(1):19—23.

[2]梁彪.羅薩和圖爾克特對盧卡西維茨多值邏輯系統的改進[J].中山大學學報論叢(社會科學版),2000,20(2):128—132.

[3]陸鐘萬.面向計算機科學的數理邏輯(第二版)[M].北京:科學出版社,2002.25—26.

[4]A.AVRON.ClassicalGentzen-typeMethodsinPropositionalMany-valuedLogics[A].BeyongTwo:TheoryandApplicationsofMulti-ValuedLogic[C].Physica-Verlag,2003.

[5]梁彪.羅薩和圖爾克特對盧卡西維茨多值邏輯系統的改進[J].中山大學學報論叢(社會科學版),2000,20(2):128—132.

[6]王禮萍,張樹功等.命題邏輯推理的代數化證明[J].計算機工程與科學,2008,30(10):78—84.

[7]陸鐘萬.面向計算機科學的數理邏輯(第二版)[M].北京:科學出版社,2002:134—136.

(責任編輯 劉洪基)

On the System Construction of the Multi-Value Logic Axiom in Lukasiewicz-based Computation Model

LIN Jiahua & JIANG Hua

(MathematicsDepartment,ChuxiongNormalUniversity,Chuxiong, 675000,YunnanProvince)

Although the classical propositional logic in theory has become mature, it is not only reliable and complete, but in the real world, not every proposition can be directly used to judge true and false. Obviously, the judgment of future events is neither true nor false proposition. In order to improve the shortcomings of classical propositional logic, based on the in-depth study of classical propositional logic, based on the Lukasiewicz model, through the extension of classical propositional logic logic truth value set, and uses the extended logic truth value assignment of proposition in lattice structure assignment. This paper puts forward six valued propositional logic system £s,systemofnegationinclassicalpropositionallogiclawofexcludedmiddle,increasethediversityofthepropositionofjudgment,itenhancestheabilityofexpressingtherealworld.

multi valued logic; formal proof; semantic constraints

楚雄師范學院校級科研項目:基于Lukasiewicz計算模型的六值命題邏輯公理體系研究。

2015 - 02 - 27

林加華(1983—),男,講師,主要研究方向:數理邏輯和信息安全。

林加華,姜 華

(楚雄師范學院信息學院,云南 楚雄 675000)

O

A

1671 - 7406(2015)06 - 0032 - 06

猜你喜歡
語義系統
Smartflower POP 一體式光伏系統
工業設計(2022年8期)2022-09-09 07:43:20
WJ-700無人機系統
ZC系列無人機遙感系統
北京測繪(2020年12期)2020-12-29 01:33:58
語言與語義
基于PowerPC+FPGA顯示系統
半沸制皂系統(下)
連通與提升系統的最后一塊拼圖 Audiolab 傲立 M-DAC mini
“上”與“下”語義的不對稱性及其認知闡釋
現代語文(2016年21期)2016-05-25 13:13:44
認知范疇模糊與語義模糊
“深+N季”組配的認知語義分析
當代修辭學(2011年6期)2011-01-29 02:49:50
主站蜘蛛池模板: 国产剧情一区二区| 国产欧美中文字幕| 精品国产成人av免费| 毛片在线播放a| 精品色综合| 婷婷成人综合| 欧美日韩精品一区二区视频| 亚洲男人的天堂在线观看| 亚洲国产午夜精华无码福利| 亚洲精品国产首次亮相| 久久天天躁夜夜躁狠狠| 日韩黄色精品| 夜精品a一区二区三区| 亚洲中文字幕手机在线第一页| 国产综合色在线视频播放线视| 国产欧美在线观看一区| a毛片免费看| 91精品国产一区| 国产精品视频999| 亚洲高清日韩heyzo| 老汉色老汉首页a亚洲| 无码人妻热线精品视频| 亚洲视频一区在线| 精品偷拍一区二区| 综合色88| 国产第八页| 久久精品免费国产大片| 91福利免费视频| 中文字幕日韩视频欧美一区| 都市激情亚洲综合久久| 亚洲天堂视频在线播放| 亚洲a级毛片| 日本成人在线不卡视频| 亚洲成人动漫在线| 欧美人与动牲交a欧美精品| 在线看AV天堂| 成人a免费α片在线视频网站| 久久久久久尹人网香蕉 | 免费人成在线观看视频色| 在线免费亚洲无码视频| 欧美日韩久久综合| 久草性视频| 看你懂的巨臀中文字幕一区二区 | 亚洲乱码在线播放| 久久综合伊人 六十路| 成人永久免费A∨一级在线播放| 成人av专区精品无码国产 | 在线看片中文字幕| 国产成人调教在线视频| 国产黄在线免费观看| 国产免费福利网站| 激情无码字幕综合| 青青草91视频| 国产成人精品视频一区视频二区| 国产精品免费久久久久影院无码| 国产va欧美va在线观看| 亚洲美女视频一区| 亚洲第一在线播放| 欧美精品在线观看视频| 国产aⅴ无码专区亚洲av综合网 | 国产91熟女高潮一区二区| 亚洲综合专区| 一本久道久久综合多人| 午夜欧美在线| 成年片色大黄全免费网站久久| 亚洲免费福利视频| 91无码视频在线观看| 免费一级大毛片a一观看不卡| 久久精品日日躁夜夜躁欧美| 精品伊人久久大香线蕉网站| 无码福利日韩神码福利片| 伊人久久综在合线亚洲91| 无码粉嫩虎白一线天在线观看| 综合天天色| 91最新精品视频发布页| V一区无码内射国产| 激情综合婷婷丁香五月尤物| 国产农村妇女精品一二区| 日韩小视频在线播放| 久久青草热| 成人无码一区二区三区视频在线观看 | 无码精油按摩潮喷在线播放|