F#: is it OK for developing theorem provers


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.

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.

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.

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#.

Best Solution

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

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.

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.