chaudhuri / sympli Goto Github PK
View Code? Open in Web Editor NEWA propositional linear inverse method theorem prover (written in 2003-2004, very lightly maintained)
License: BSD 2-Clause "Simplified" License
A propositional linear inverse method theorem prover (written in 2003-2004, very lightly maintained)
License: BSD 2-Clause "Simplified" License
Compiling ========= This requires the MLTon version 20130715 or later. It currently does not work with SML/NJ. You will need the mlyacc-lib library as well, which is generally distributed with the mlton-basis package. Running the MLTon compiled binary ================================= Running "make" produces a program "sym". Use it as follows: % ./sym [-e #] file1.sym file2.sym ... It runs the files one after the other. The -e option specifies which search engine to use. The engines and their numbers are in top/engine.sml. If you are trying one of the profiled binaries (eg. sym-time), perform the following steps in order: % ./sym-time file1.sym file2.sym ... % mlprof -raw true ./sym-time mlmon.out The "-raw true" flag shows raw values in addition to the percentage values. If you want source line numbers also, use "-show-line true". Input format ============ 1. Comments ------------- Block comments are delimited by balanced (* and *). They may be arbitrarily nested. Line comments start with '% ' (minus quotes), and ignore everything until the end of line character. 2. Propositions ----------------- Any identifier that is not a keyword is a valid atomic proposition. Propositions are combined with the following unary and binary connectives, listed in order of precedence: ! exponential * tensor, left assoc. & with, left assoc. + choice, left assoc. -o linear impl., right assoc. o- linear impl., left assoc. (B o- A == A -o B) -> implication, right assoc. (A -> B == !A -o B) <- implication, left assoc. (B <- A == !A -o B) o-o linear equiv., non assoc. (A o-o B == (A -o B) & (A o- B)) <-> unr. equiv., non assoc. (A <-> B == (A -> B) & (A <- B)) { } CLF-monad In addition are the propositional constants 0, 1 and #. 0 falsehood 1 unit (mult.) # truth (add.) 3. Proof terms ---------------- Proofs are represented as normal natural deduction terms. They have the following grammar. (synthesizing) i ::| u hypothesis | i c impl elim | fst i | snd i with elims | [c] coercion (checking) c ::| i silent coercion | c * c tensor intro | let u * v = i in c end tensor elim | 1 one intro | let 1 = i in c end one elim | \u. c impl intro | (c, c) with intro | () top intro | inl c | inr c choice intros | case i of inl u => c | inr u => c choice elim | abort i zero elim | !c bang intro | let !u = i in c end bang elim | {c} monad intro | let {u} = i in c end monad elim | let u = i in c end delayed linear subst | ulet w = i in c end delayed unrestr. subst Proof terms with the [] coercion are not normal, and cannot be checked. Non-normal proof terms are produced during the proof-maintenance phase, but they are normalized before checking. NOTE TO USERS OF NON-MONADIC VERSION: The CLF monad is written using {}. This is different from the {} coercion of earlier versions. 4. Directives --------------- All directives are prefixed by '%', with no following space. They are as follows. %prove <prop>. Proves a the given proposition, and: %refute [<number> :] <prop>. Attempt to perform <number> (default: infinite) iterations for the OTTER loop, and then succeeds; but fail if a proof is found. %include 'filename.sym'. Process named file. %norm <checking>. Take the given closed checking term and calculate its beta-gamma-normal form. %check <checking> : <prop>. %reject <checking> : <prop>. Check (or reject) a given closed *normal* proof term against a given proposition. Attempts to check (reject) a term containing [] will always fail (succeed). %channel <channel>. Allocates a new channel of output, and binds it to standard out. Channel names are any valid identifier. By default there are two channels: 'highlevel' and 'error', both bound to the standard out. %bind <channel> : 'somefilename.log'. Send all output to specified channel from now on to somefilename.log. The channel need not have been specified with %channel earlier. You can rebind channels, in which case the old file (if any) that the channel was bound to is closed. NOTE: if you bind to a file twice in one run, you'll end up overwriting all the output of the first run %log <operation> : <channel>. Log the specified operation on the specified channel. Operation names are valid identifiers. The following are the documented operations: cfg -- output produced while reading the input file and delegating to various components. This is on 'highlevel' by default. setup -- during a proof or a refute, this prints the various setup and teardown steps such as the calculated labels, initial sequents, goal, etc. Not on anything by default. rules -- all output during specialising of rules. Not on anything by default. counters -- various performance and statistics counters. Not on anything by default. database -- the kept sequents at the beginning of every OTTER loop. Not on anything by default. sos -- the set of support at the beginning of every OTTER loop. Not on anything by default. active -- the active set at the beginning of every OTTER loop. Not on anything by default. sel -- the selected sequent at the beginning of every OTTER loop. Not on anything by default. prefactor, postfactor -- new sequents before and after factoring. Not on anything by default. fsubs, bsubs -- forward and backward subsumption output. Not on anything by default. validation -- output produced by the final validation phase, including the final proof-term. Not on anything by default. loop -- misc. output specific to the mechanics of the OTTER loop. Not on anything by default. timers -- various timers, printed at the end of major commands and directives (i.e., prove, refute, %check, %reject, etc.) NOTE: there is no additional cost to operations that are not logged on anything. %unlog <operation>. Stop logging the specified operation.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.