dfg2dfg - 클라우드에서 온라인

프로그램:

이름

dfg2dfg - 문제의 근사값을 계산합니다

개요

dfg2dfg [-혼] [-모나딕] [-선형] [-얕은] [인파일] [아웃파일]

기술

dfg2dfg DFG 구문으로 입력 파일에서 절을 읽는 프로그램입니다. 그런 다음
명령줄 옵션에 따라 절 집합의 근사값을 계산합니다.
마지막으로 DFG 구문으로 설정된 근사 절을 파일에 씁니다.

둘 다 인파일 ...도 아니다 아웃파일 주어진다, dfg2dfg 표준 입력에서 읽고 씁니다.
표준 출력. 파일 이름이 하나 지정되면 해당 파일에서 읽고 출력을 씁니다.
표준 출력으로. 파일 이름이 두 개 이상 지정되면 dfg2dfg 첫 번째부터 읽습니다
파일을 두 번째에 씁니다.

근사값은 별도 논문에 기술적으로 자세히 설명되어 있습니다. dfg2dfg.ps
SPASS 배포판에 포함됨.

옵션

dfg2dfg 결합할 수 있는 네 가지 명령줄 옵션이 있습니다.

-뿔
이 옵션을 사용하면 혼절이 아닌 절을 혼절로 변환할 수 있습니다. 각
비뿔 조항 n 긍정적인 리터럴은 다음으로 변환됩니다. n 뿔절, 여기서
i-th 절에는 다음이 포함됩니다. i-번째 긍정적 리터럴과 모든 부정적 리터럴(비-)
horn clause. 본 논문의 3절도 참조하세요.

-모나딕[=n]
이 옵션을 사용하면 비모나딕 술어 기호가 있는 원자가 모나딕으로 변환됩니다.
원자. 만약 n 생략되거나 n=1 용어 인코딩이 적용됩니다. 즉, 모든 비모나딕
술어는 용어 수준으로 이동됩니다. n=2 투영이 적용됩니다. 모든 비
모나드 원자는 모나드 인수 투영으로 대체됩니다. 4.1절을 참조하세요.
자세한 내용은 논문의 4.2절을 참조하세요.

-선의
이 근사화는 모나딕 리터럴과 비선형 변수를 포함하는 절을 변환합니다.
후속 원자에서의 발생은 더 부정적인 의미를 갖는 새로운 절로 변환됩니다.
리터럴은 succedent에 비선형 변수를 포함하지 않습니다. 섹션을 참조하세요.
자세한 내용은 논문 5쪽을 참조하세요.

-얕은[=n]
이 변환은 긍정 리터럴에서 용어의 깊이를 줄이려고 시도합니다.
변환은 모나딕 리터럴이 있는 호른 절에만 적용됩니다. n 생략
or n=1 엄격한 변환이 적용되므로 동등성은 유지됩니다.
럭셔리 n=2 일부 전제 조건이 제거되었습니다. 이를 통해 변환을 적용할 수 있습니다.
더 자주, 하지만 변환은 더 이상 동등성을 보존하지 않습니다. n=3
더 많은 전제 조건이 제거되었습니다. 6절을 살펴보세요.n 논문의
명령줄 옵션의 세부 정보 -모나딕=n.

onworks.net 서비스를 사용하여 dfg2dfg를 온라인으로 사용하세요