F#:可以开发定理证明吗？

请指教.我是一名律师,我在法律信息学领域工作.我很长一段时间都是程序员(Basic,RPG,Fortran,Pascal,Cobol,VB.NET,C#).我目前对F#感兴趣,但我想要一些建议.我担心的是F#似乎适合数学应用.而我想要的是需要大量的布尔数学运算和文本的自然语言处理,如果成功,还需要语音.我担心文本处理.

我收到了革命性的PROLOG源代码(法律领域的革命,特别是争议解决).该计划通过评估两个辩论方提出的是 - 否(真假)论点来解决争议.现在,我正在学习PROLOG,所以我可以将程序提升到另一个层次:当它们既不是是或否时,评估论证的强度,但在论证过程中是一个有说服力的元素.

因此,该程序处理论证的辩证法方面,我希望它开始处理论证的修辞方面,或至少某些方面.

目前该程序可以管理形式逻辑.我想要的是开始管理非正式逻辑的某些方面,为此我需要解析字符串(长字符串,可能是ms字文档)来检测文本标记,像"但是""因此""然而"这样的单词"自"等等,只需要在任何语音(口头或书面)和标记中查找一长串单词,然后评估标记的左侧和右侧.根据标记,两侧被视为强或弱.

最初,我想到将Prolog程序移植到C#并使用Prolog库.然后,它对我来说也许它可能在纯F#中更好.

首先,你描述的项目听起来(我相信这是正确的法律术语)完全令人敬畏.

其次,虽然F#是数学应用程序的不错选择,但它也非常适合执行大量符号处理的任何应用程序.值得注意的是,F#是ML系列语言的一部分,最初是为了开发定理证明的特定目的而设计的.听起来你正在编写一个直接吸引小众ML语言的应用程序.

我个人建议编写任何证明你在F#而不是C#中使用的定理的定理 - 只是因为得到的F#代码大约是C#等价的1/10.我发布了这个示例,演示如何评估C#和F#中的命题逻辑,你可以看到自己的差异.