분리형 정규형 수식

Question

Im 대칭 일반형으로 수식의 집합 기반 표현을 사용하려고합니다. 그리고 함께이 교환 법칙, 결합 및 (A ∧ a)는 그것과 동일이기 때문에 편리 리터럴의 그것의 세트 litOf (BC)에 의해 기본 결합한 BC을 나타낸다는 것을 발견했습니다.

BC1의 V하십시오 논리합 정규형 공식 을 나타내는 생각

임. . . V 세트에 의해

BCN :

dnfToSet(a) = {litOf(bc1), . . . , litOf(bcn)} 

우리는의 DNS 설정을 호출 할 것이다.

어떻게 기능 및 dnfToSet litOf 에 대한 F 번호 선언을 작성해야?

Answer 1

는 제가 질문을 이해 모르겠지만, 여기에 내가 생각 해낸 것입니다 :

이

let litOf = Set.ofSeq 
let dnfToSet a = 
    let isNotSuperset bci = a |> Set.forall(fun bcj -> (bci = bcj) || not(Set.isSuperset bci bcj)) 
    a |> Set.filter isNotSuperset 

다음은 보여

type bc = A | B | C | D 

let bc1 = litOf [A; B; C] 
let bc2 = litOf [B; C; B] 
let bc3 = litOf [C; B; A] 
let bc4 = litOf [D] 
let a = litOf [ bc1; bc2; bc3; bc4 ] 
let dnf = dnfToSet a 

FSI 수익률로 모든 퍼팅 :

type bc = 
    | A 
    | B 
    | C 
    | D 
val bc1 : Set<bc> = set [A; B; C] 
val bc2 : Set<bc> = set [B; C] 
val bc3 : Set<bc> = set [A; B; C] 
val bc4 : Set<bc> = set [D] 
val a : Set<Set<bc>> = set [set [A; B; C]; set [B; C]; set [D]] 
val dnf : Set<Set<bc>> = set [set [B; C]; set [D]] 

((B ∧ C) V (D)) 

마지막으로 레코드의 경우 공식을 인쇄하는 데 사용한 함수는 다음과 같습니다.

let sprintlit lit = 
    System.String.Join(" ∧ ", lit |> Seq.map(sprintf "%A") |> Seq.toArray) 
    |> sprintf "(%s)" 

let sprintdnf set = 
    System.String.Join(" V ", set |> Seq.map sprintlit |> Seq.toArray) 
    |> sprintf "(%s)"