F#:可以开发定理证明吗? [英] F#: is it OK for developing theorem provers?

问题描述

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

Please advise. I am a lawyer, I work in the field of Law Informatics. I have been a programmer for a long time (Basic, RPG, Fortran, Pascal, Cobol, VB.NET, C#). I am currently interested in F#, but I'd like some advise. My concern is F# seems to be fit for math applications. And what I want would require a lot of Boolean Math operations and Natural Language Processing of text and, if successful, speech. I am worried about the text processing.

我收到了革命性的PROLOG源代码(法律领域，尤其是争议解决领域的革命).该程序通过评估两个辩论方提出的是-否(对-错)论点来解决争端.现在，我正在学习PROLOG，以便将程序带入另一个层次:当参数不是Yes或No而是论证过程中具有说服力的元素时，评估论点的强度.

I received a revolutionary PROLOG source code (revolutionary in the field of Law and in particular Dispute Resolution). The program solves disputes by evaluating Yes-No (true-false) arguments advanced by two debating parties. Now, I am learning PROLOG so I can take the program to another level: evaluate the strenght of arguments when they are neither a Yes or No, but a persuasive element in the argumentation process.

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

So, the program handles the dialectics aspect of argumentation, I want it to begin processing the rhetoric aspect of argumentation, or at least some aspects.

当前程序可以管理形式逻辑.我想要的是开始管理非正式逻辑的某些方面，为此，我需要对字符串(长字符串，可能是ms单词文档)进行解析以检测文本标记，例如"but"，"there"，"however"等单词. 自"等等等，我只需要在任何语音(口头或书面)中查找并标记一个长长的单词，然后评估标记的左侧和右侧.根据标记的不同，侧面被认为是坚固的或脆弱的.

Currently the program can manage formal logic. What I want is to begin managing some aspects of informal logic and for that I would need to do parsing of strings (long strings, maybe ms word documents) for the detection of text markers, words like "but" "therefore" "however" "since" etc, etc, just a long list of words I have to look up in any speech (verbal or written) and mark, and then evaluate left side and right side of the mark. Depending on the mark the sides are deemed strong or weak.

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

Initially, I thought of porting the Prolog program to C# and use a Prolog library. Then, it ocurred to me maybe it could be better in pure F#.

推荐答案

首先，您描述的项目听起来(我相信这是正确的法律用语)完全令人震惊.

First, the project you describe sounds (and I believe this is the correct legal term) totally freaking awesome.

第二，虽然F#是数学应用程序的不错选择，但它也非常适合于执行大量符号处理的任何应用程序.值得注意的是，F#是ML语言系列的一部分，该语言最初是为开发定理证明者的特定目的而设计的.听起来您正在编写的应用程序直接吸引了面向特定市场的ML语言.

Second, while F# is a good choice for math applications, its also extremely well-suited for any applications which perform a lot of symbolic processing. Its worth noting that F# is part of the ML family of languages which were originally designed for the specific purpose of developing theorem provers. It sounds like you're writing an application which appeals directly to the niche ML languages are geared for.

我个人建议使用F#而不是C#编写任何具有定理证明的应用程序-仅因为生成的F#代码大约是C#等效代码的1/10.我发布了此示例演示了如何在C#和F#中评估命题逻辑，您可以自己了解差异.

I would personally recommend writing any theorem proving applications you have in F# rather than C# -- only because the resulting F# code will be about 1/10th the size of the C# equivalent. I posted this sample demonstrating how to evaluate propositional logic in C# and F#, you can see the difference for yourself.

这篇关于F#:可以开发定理证明吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！