| 210f743 | Olivier ROLAND | 17 February 2013, 17:40:36 UTC | Other neccessary changes to mvn clean install gapt with no errors | 17 February 2013, 17:40:36 UTC |
| 6e6e291 | Olivier ROLAND | 22 November 2012, 18:38:41 UTC | Mofifications needed for Scala 2.10 to mvn clean install gapt with no errors | 22 November 2012, 18:38:41 UTC |
| dbc22b4 | Olivier ROLAND | 16 November 2012, 23:12:10 UTC | Yet another fix for m2e integration | 16 November 2012, 23:14:12 UTC |
| 3e3b823 | Olivier ROLAND | 16 November 2012, 18:22:44 UTC | Merge branch 'm2e' of ssh://github.com/newca12/gapt into m2e | 16 November 2012, 18:22:44 UTC |
| 0706eb1 | Olivier ROLAND | 31 October 2012, 16:27:33 UTC | Fix m2e integration | 16 November 2012, 18:21:26 UTC |
| b031d29 | mrukhaia | 16 November 2012, 15:40:05 UTC | Button for Herbrand Sequent extraction is added to ProofTool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1300 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 16 November 2012, 15:40:05 UTC |
| d039ec7 | Martin.Riener | 15 November 2012, 17:10:43 UTC | hotfix to prover9 proof import to circumvent a bug in prooftrans git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1299 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 November 2012, 17:10:43 UTC |
| e14baee | mrukhaia | 15 November 2012, 14:22:33 UTC | Skolemization, regularization and Ivy parser is added to ProofTool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1298 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 November 2012, 14:22:33 UTC |
| 3ace96a | mrukhaia | 12 November 2012, 14:10:16 UTC | Fixed some problems with cl variables. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1297 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 12 November 2012, 14:10:16 UTC |
| 227cd30 | cdunchev@gmail.com | 11 November 2012, 20:28:32 UTC | During the last project meeting Alex proposed to replace the cl^{(proof, \Omega)} symbols in the displaying with symbols which do not contain the useless for the user information such as proof name and omega-configuration. Now they are replaced with unique HOLConsts of type \omega -> o git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1296 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 11 November 2012, 20:28:32 UTC |
| 02d7937 | mrukhaia | 11 November 2012, 16:15:01 UTC | Handling of nested quantifiers in ExpansionTree is corrected in ProofTool. One such test is added in the Test menu. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1295 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 11 November 2012, 16:15:01 UTC |
| 978a858 | cdunchev@gmail.com | 11 November 2012, 14:13:31 UTC | A small bug in struct extraction is fixed. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1294 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 11 November 2012, 14:13:31 UTC |
| 60c7765 | stefan.hetzl@gmail.com | 09 November 2012, 18:21:55 UTC | typo git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1293 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 09 November 2012, 18:21:55 UTC |
| b2f741b | giselle.mnr@gmail.com | 08 November 2012, 15:27:54 UTC | Fixes issue 206. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1292 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 November 2012, 15:27:54 UTC |
| a475435 | cdunchev@gmail.com | 08 November 2012, 14:26:45 UTC | A new test for the schema projection term has been added. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1291 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 November 2012, 14:26:45 UTC |
| 5613a6f | Martin.Riener | 07 November 2012, 22:11:29 UTC | parsing of paramod and flip works now, translation to robinson proofs is still buggy git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1290 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 07 November 2012, 22:11:29 UTC |
| 729af9d | mrukhaia | 07 November 2012, 15:45:16 UTC | ExpansionTrees improved: single instance is drawn inside <> as well and left mouse clicking is added to open/expand a quantifier. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1289 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 07 November 2012, 15:45:16 UTC |
| eceea7b | cdunchev@gmail.com | 05 November 2012, 20:52:16 UTC | Meanwhile another bug was found and fixed. The projection extraction, instantiation and unfolding can be seen also in ProofTool for arbitrary instance. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1288 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 05 November 2012, 20:52:16 UTC |
| 679be28 | cdunchev@gmail.com | 05 November 2012, 12:59:24 UTC | two examples were modified. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1287 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 05 November 2012, 12:59:24 UTC |
| 57b5840 | cdunchev@gmail.com | 05 November 2012, 00:27:07 UTC | The bug in the unfolding of normalized projection terms was fixed. Wieder alles in Ordnung. :) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1286 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 05 November 2012, 00:27:07 UTC |
| bed0691 | Martin.Riener | 04 November 2012, 15:10:32 UTC | fixed naming scheme for ivy parser - GEO037-2.ivy is still not parsable because it contains a paramodulation step (halfway implemented but still buggy and without translation to robinson resolution) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1285 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 04 November 2012, 15:10:32 UTC |
| 4b149fa | cdunchev@gmail.com | 04 November 2012, 04:29:20 UTC | In my previous comment, in the ProjectionTerm.scala there was a "TODO:" gap in the UnfoldProjectionTerm object. Now it is implemented. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1284 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 04 November 2012, 04:29:20 UTC |
| 2103d18 | mrukhaia@gmail.com | 03 November 2012, 21:29:21 UTC | A typo. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1283 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 03 November 2012, 21:29:21 UTC |
| e7793dc | mrukhaia@gmail.com | 03 November 2012, 21:22:01 UTC | Instantiation of ProjectionTerm schema is integrated in prooftool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1282 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 03 November 2012, 21:22:01 UTC |
| b300728 | cdunchev@gmail.com | 01 November 2012, 21:56:56 UTC | The set of all proof projections is extracted from the normalized (grounded) projection term. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1281 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 01 November 2012, 21:56:56 UTC |
| 8dbe722 | shaolintl@gmail.com | 31 October 2012, 22:47:02 UTC | 1) created MultiExpansionTree which is the same as ExpansionTree but allow for vectors of selected/expanded terms 2) created an algorithm which compresses a tree into a multiTree for sequential quantifiers of the same type 3) added the relevant method to cli git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1280 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 31 October 2012, 22:47:02 UTC |
| bb95090 | Martin.Riener | 31 October 2012, 21:35:33 UTC | loadProver9Proof in the cli now parses prover9 output, the new prover9(filename : String) refutes a file given in ladr format (have to find a better name for this) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1279 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 31 October 2012, 21:35:33 UTC |
| f96d9e6 | Olivier ROLAND | 31 October 2012, 16:27:33 UTC | Fix m2e integration | 31 October 2012, 16:33:46 UTC |
| 727dce5 | giselle.mnr@gmail.com | 30 October 2012, 16:39:32 UTC | Reverting changes that did not fix issue 206. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1278 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 30 October 2012, 16:39:32 UTC |
| 769cb79 | Martin.Riener | 29 October 2012, 18:43:58 UTC | fixed transformation from ivy resolution to robinson resolution. shared nodes were duplicated which is a problem in the case of GRA014+1: the prover9 refutation has 210 inferences, the ivy refutation has 479 and the ground refutation has 18042747 git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1277 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 29 October 2012, 18:43:58 UTC |
| a9265d8 | mrukhaia | 29 October 2012, 16:09:12 UTC | ExpansionTrees can be expanded now. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1276 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 29 October 2012, 16:09:12 UTC |
| e781ecb | Martin.Riener | 29 October 2012, 11:48:50 UTC | ivy parser performance should be acceptable now - tests go through in 3s now git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1275 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 29 October 2012, 11:48:50 UTC |
| f9aa5c1 | cdunchev@gmail.com | 28 October 2012, 23:45:05 UTC | Grounding a schematic projection term for a given instance and unfolding the term. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1274 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 October 2012, 23:45:05 UTC |
| 91a61ca | mrukhaia@gmail.com | 28 October 2012, 18:58:06 UTC | First attempt to expand ExpansionTrees. Also some bugs fixed and test proofs added. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1273 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 October 2012, 18:58:06 UTC |
| 565e689 | Martin.Riener | 28 October 2012, 02:58:21 UTC | replaced SExpression parser by a more efficient one. example GRA014+1.ivy can now be read, but it still takes 20s to load - need to improve git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1272 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 October 2012, 02:58:21 UTC |
| 48853d5 | mrukhaia@gmail.com | 27 October 2012, 17:26:40 UTC | ExpansionTrees can be opened/closed now. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1271 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 October 2012, 17:26:40 UTC |
| 5531d31 | mrukhaia@gmail.com | 26 October 2012, 17:28:47 UTC | Got annoyed with syntax warning messages. Now all these files follow scala conventions. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1270 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 October 2012, 17:28:47 UTC |
| 309a6c8 | mrukhaia | 25 October 2012, 16:49:42 UTC | Only the first quantifiers in a formula can be opened-closed so far. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1269 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 25 October 2012, 16:49:42 UTC |
| 0ed22e0 | Martin.Riener | 25 October 2012, 15:52:06 UTC | connected the prover9 interface to the ivy parser. Prover9.refute now returns an Option[RobinsonResultion] so you can extract the proof(in case of parsing errors a trivial proof of the empty sequent will be given). use replay(clauses) in the cli to use the replay method, use prover9(clauseset) for the ivy translation and use loadProver9Proof will load a prover0 ouptut file without running prover9. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1268 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 25 October 2012, 15:52:06 UTC |
| 377ec17 | Martin.Riener | 25 October 2012, 13:30:55 UTC | forgot factor (propositional) rule in ivy proofs git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1267 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 25 October 2012, 13:30:55 UTC |
| bd9a213 | mrukhaia | 24 October 2012, 14:20:57 UTC | First attempt to display expansion trees. The problem with parenthesis solved: all of them look the same, but some of them (the ones over the binary connectives) are clickable and can be marked with different colors. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1266 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 24 October 2012, 14:20:57 UTC |
| 6d07ae9 | Martin.Riener | 24 October 2012, 11:24:50 UTC | added translation from IvyResolution to RobinsonProofWithInstance; you can try it out by pasting prooftool(Robinson2LK(loadIvyProof("provers/prover9/src/test/resources/manyliterals.ivy"))) into the cli (path relative to the gapt/source directory) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1265 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 24 October 2012, 11:24:50 UTC |
| 2920092 | shaolintl@gmail.com | 24 October 2012, 09:28:00 UTC | added support for robinson resolution proofs with an instantiation rule and integrated such a proof into the resolution to LK algorithm. Martin, please try to use it and tell me if it does not work as expected. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1264 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 24 October 2012, 09:28:00 UTC |
| e968490 | Martin.Riener | 23 October 2012, 19:00:53 UTC | parsing of paramodulution-free ivy proofs works now, the cli has a new command loadIvyProof(filename:String) -- prooftool does not display aribtrary AGraphProofs, need to fix that git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1263 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 23 October 2012, 19:00:53 UTC |
| 9fc601c | mrukhaia | 22 October 2012, 14:40:08 UTC | Sorry, forgot the pom file. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1262 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 22 October 2012, 14:40:08 UTC |
| 33b1018 | mrukhaia | 22 October 2012, 14:38:47 UTC | Some preparatory work for Expansion Tree Viewer. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1261 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 22 October 2012, 14:38:47 UTC |
| 4fdbce1 | Martin.Riener | 19 October 2012, 17:58:20 UTC | partial commit of ivy resolution calculus (split from resolution calculus because direct creation of robinson resolution proofs is too complicated) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1260 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 19 October 2012, 17:58:20 UTC |
| b092ab9 | shaolintl@gmail.com | 16 October 2012, 11:38:02 UTC | changed expansion trees to have their own structure in calculi. the method in cli now returns a pair or seq of expansion trees git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1259 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 16 October 2012, 11:38:02 UTC |
| 520ba3c | shaolintl@gmail.com | 15 October 2012, 08:03:11 UTC | Fixed a bug with regard to weakening rules in the expanion trees extraction algorithm git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1258 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 October 2012, 08:03:11 UTC |
| 7dadce2 | shaolintl@gmail.com | 12 October 2012, 22:01:43 UTC | and another small thing I forgot to change before git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1257 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 12 October 2012, 22:01:43 UTC |
| 77faf2d | shaolintl@gmail.com | 12 October 2012, 21:47:02 UTC | My apologizes. I did not know the fold method in trees is used (I thought it incorrect) and I removed it. I have returned it now. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1256 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 12 October 2012, 21:47:02 UTC |
| c23409a | shaolintl@gmail.com | 12 October 2012, 21:29:19 UTC | fixes issue 208 added call extractExpansionTrees(lkProof) to cli with returns a pair of seqs of TreeA objects added also another tree data structure (in ds.algebraic.trees) and both tree datastructures are now implementing the TreeA interface (from ds.trees) Mikheil, I have added extractors for working with the new data structure and if you are working with trees in ProofTool and not with proofs, then you should use the new abstraction. A note, due to a lack of time I could not test it except running it on the following simple example in cli: val seq = FSequent(List(parse.fol("P(a)"),parse.fol("Forall x Imp P(x) P(f(x))")),List(parse.fol("P(f(f(a)))"))) val c1 = FSequent(List(parse.fol("P(x)")),List(parse.fol("P(f(x))"))) val c2 = FSequent(List(parse.fol("P(f(f(a)))")),List()) val c3 = FSequent(List(),List(parse.fol("P(a)"))) val resProof = refuteFOL(List(c1,c2,c3)) val lkProof = Robinson2LK(resProof.get, seq) val expTrees = extractExpansionTrees(lkProof) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1255 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 12 October 2012, 21:29:19 UTC |
| 41b7bd6 | shaolintl@gmail.com | 12 October 2012, 16:02:56 UTC | There was a weird definition of BinaryFormula in syntax/hol, which tried to pattern match also Equations. Since they are Atoms, it might have caused to some runetime errors. I am commiting it without doing a full test of the project as I believe it can break only tests and in this case, the tests are wrong. If I am wrong, I apologize in advance. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1254 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 12 October 2012, 16:02:56 UTC |
| db0b12c | giselle.mnr@gmail.com | 12 October 2012, 15:21:32 UTC | Attempt to fix issue 206 git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1253 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 12 October 2012, 15:21:32 UTC |
| f716c64 | shaolintl@gmail.com | 11 October 2012, 13:45:46 UTC | added support for implication for computing projections. straightforward but not tested. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1252 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 11 October 2012, 13:45:46 UTC |
| 7e9d939 | Martin.Riener | 10 October 2012, 17:35:55 UTC | added parser for a subset lisp s-expressions, should be enough to parse ivy files git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1251 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 10 October 2012, 17:35:55 UTC |
| f63154b | shaolintl@gmail.com | 08 October 2012, 15:08:36 UTC | fixed issue 207. using Giselle's clean structural rules and adding contractions in order to obtain the intended end sequent git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1250 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 October 2012, 15:08:36 UTC |
| b6f8aff | giselle.mnr@gmail.com | 08 October 2012, 12:05:49 UTC | Optimizations in autoprop. Now unary rules are solved before binary rules. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1249 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 October 2012, 12:05:49 UTC |
| 014cd6d | cdunchev@gmail.com | 08 October 2012, 02:43:12 UTC | ;) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1248 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 October 2012, 02:43:12 UTC |
| 2ed68b2 | cdunchev@gmail.com | 08 October 2012, 02:15:38 UTC | ;) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1247 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 October 2012, 02:15:38 UTC |
| 0983825 | cdunchev@gmail.com | 08 October 2012, 00:37:26 UTC | A test for auto-propositional has been added in the integration tests. The name of the object cleanStructuralRules coincided with the name of a private function cleanStructuralRules(...) and strangely this caused a problem, so I renamed the object to CleanStructuralRules. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1246 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 October 2012, 00:37:26 UTC |
| c1349c1 | giselle.mnr@gmail.com | 06 October 2012, 22:36:56 UTC | Fixes issue 205. Also, changed the package of autoprop to algorithms/lk. It was renamed to solvePropositional (just to avoid conflicts as I was modifying... I can rename it back if somebody wants it. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1245 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 06 October 2012, 22:36:56 UTC |
| ef127b7 | mrukhaia@gmail.com | 06 October 2012, 22:05:19 UTC | In expansion tree now only quantifiers are "clickable". git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1244 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 06 October 2012, 22:05:19 UTC |
| 28485be | stefan.hetzl@gmail.com | 06 October 2012, 11:57:31 UTC | two more example proof sequences (primarily for cut-introduction) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1243 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 06 October 2012, 11:57:31 UTC |
| 4d40ae8 | giselle.mnr@gmail.com | 03 October 2012, 15:11:50 UTC | Added documentation for the exportXL function. Printing the number of total rules when printProofStats is called. Deleted a file that was all commented out. Improved the prunning of redundancies in propositional proofs. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1242 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 03 October 2012, 15:11:50 UTC |
| 83c5ad3 | fraini | 01 October 2012, 11:22:03 UTC | Added hol2fol to the CLI. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1241 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 01 October 2012, 11:22:03 UTC |
| 18e0627 | giselle.mnr@gmail.com | 30 September 2012, 11:45:11 UTC | Fixing pom after previous delete git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1240 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 30 September 2012, 11:45:11 UTC |
| edfbd72 | giselle.mnr@gmail.com | 30 September 2012, 11:21:21 UTC | Removing useless class git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1239 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 30 September 2012, 11:21:21 UTC |
| ad98fe7 | mrukhaia@gmail.com | 29 September 2012, 22:54:41 UTC | Elimination of structural rules extended with missing rules and reductive cut-elimination procedure improved by that function. Also small bugs fixed in prooftool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1238 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 29 September 2012, 22:54:41 UTC |
| 650b2c0 | giselle.mnr@gmail.com | 29 September 2012, 10:04:06 UTC | Changing the name of a class to fix compilation in MacOS. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1237 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 29 September 2012, 10:04:06 UTC |
| 910c8e9 | mrukhaia | 28 September 2012, 18:20:06 UTC | Small changes for Giselle again, to exit prooftool from cli without exiting cli itself (from File>Exit or ctrl+X). git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1236 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 September 2012, 18:20:06 UTC |
| 58f61fc | giselle.mnr@gmail.com | 28 September 2012, 16:48:16 UTC | Added function to count the number of quantified rules and total number of rules to the statistics package. Added the code to remove redundant weakenings and contractions to elimination package and extended it to arbitrary proofs (before it worked only for propositional cut-free proofs). Removed some useless printing from the cut-introduction algorithm. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1235 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 September 2012, 16:48:16 UTC |
| e6214fc | mrukhaia | 28 September 2012, 15:57:57 UTC | Small changes for Giselle to view Herbrand sequent from cli via prooftool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1234 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 September 2012, 15:57:57 UTC |
| c17bcae | cdunchev@gmail.com | 28 September 2012, 14:58:05 UTC | This example has been fixed. The clause set and the projection term now work. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1233 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 September 2012, 14:58:05 UTC |
| fbb6667 | giselle.mnr@gmail.com | 27 September 2012, 17:13:26 UTC | - Fixed algorithm for removing redundant weakenings and contractios after autoprop. Now proofs returned by this method are already without these structural redundancies. - Implemented a class for extended herbrand sequent (one cut case) - Implemented a class for decompositions (one cut case), but I am not yet using on the current code. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1232 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 September 2012, 17:13:26 UTC |
| c882f33 | mrukhaia@gmail.com | 26 September 2012, 21:42:11 UTC | Fixes issue 159 (structural rules can be hidden in prooftool) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1231 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 September 2012, 21:42:11 UTC |
| 89923bd | mrukhaia | 26 September 2012, 17:44:28 UTC | Proof can be split in prooftool. Right-click on a sequent in a proof and choose corresponding menu item. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1230 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 September 2012, 17:44:28 UTC |
| 442aa2c | mrukhaia | 26 September 2012, 17:23:07 UTC | Subproof can be hidden in prooftool. Right-click on a sequent in a proof and choose corresponding menu item. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1229 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 September 2012, 17:23:07 UTC |
| 7e523cf | mrukhaia | 26 September 2012, 14:00:44 UTC | Fixes issue 204. (bug in macro rules) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1228 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 September 2012, 14:00:44 UTC |
| 1603735 | giselle.mnr@gmail.com | 25 September 2012, 16:53:45 UTC | Implemented CNF transformation (tests needed). Started the simplification of the canonical solution for the cut-introduction algorithm. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1227 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 25 September 2012, 16:53:45 UTC |
| 18c108a | mrukhaia | 25 September 2012, 15:31:48 UTC | Fixed problem with resizing expansion trees. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1226 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 25 September 2012, 15:31:48 UTC |
| d617189 | cdunchev@gmail.com | 25 September 2012, 14:36:46 UTC | Some working tests. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1225 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 25 September 2012, 14:36:46 UTC |
| fa63129 | giselle.mnr@gmail.com | 24 September 2012, 16:31:58 UTC | Cut-introduction algorithm now builds the entire proof using Autoprop. A function for transposing matrices was added to Utils. The code for using interpolation is implemented but commented out, since there's still a bug. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1224 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 24 September 2012, 16:31:58 UTC |
| 9c6abef | stefan.hetzl@gmail.com | 22 September 2012, 10:05:24 UTC | spelling git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1223 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 22 September 2012, 10:05:24 UTC |
| 7c4a533 | giselle.mnr@gmail.com | 21 September 2012, 15:43:39 UTC | Put the substitution methods in FOLFormula. Now you can substitute a term t in a FOL formula f using: f.substitute(t) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1222 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 September 2012, 15:43:39 UTC |
| 171c15c | giselle.mnr@gmail.com | 21 September 2012, 14:38:12 UTC | Added function to check if a formula is prenex. Now the term extraction algorithm throws an exception if not all formulas from the end-sequent are prenex. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1221 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 September 2012, 14:38:12 UTC |
| 37e4338 | giselle.mnr@gmail.com | 21 September 2012, 09:09:33 UTC | Fixing Herbrand Extraction tests. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1220 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 September 2012, 09:09:33 UTC |
| 978bd3f | giselle.mnr@gmail.com | 20 September 2012, 22:06:36 UTC | Added herbrand sequent extraction function to the top level and documented it. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1219 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 20 September 2012, 22:06:36 UTC |
| 32eaa5a | shaolintl | 20 September 2012, 18:25:19 UTC | - added isAncestor to FormulaOccurrence - added WeakeningsElimination algorithm that removes all formulas in the end sequent of a proof if they originated in weakenings - use this algorithm in the robinsonToLK algorithm since we multiple formulas in the end sequent by using weakenings. Important! we might need to add weakenings at the end if end formulas which are needed are inserted using weakenings. I am not sure it can happen in robinsonToLK though. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1218 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 20 September 2012, 18:25:19 UTC |
| c8607b0 | shaolintl | 19 September 2012, 13:23:37 UTC | added to CLI.Robinson2LK the option to accept a sequent and returns an LK proof of the sequent 's' based on the resolution proof if the resolution proof is obtained from clauses in CNF(-s) issues: - Imp(right and left) is not supported and should be added (simple exercise) - there are redundancy occurring due to the multipicative nature of the calculus. in binary rules I duplicate the context formulas. This can be handled either by: -- postprocessing - either add contractions or cancel contractions with weakenings -- inprocessing but pretty complex a simple example (forall x P(x) |- P(a)): al f1 = parse.fol("Forall x P(x)") val Pa = parse.fol("P(a)") val Px = parse.fol("P(x)") val resProof = refuteFOL(List(FSequent(List(Pa),List()),FSequent(List(),List(Px)))) val seq = FSequent(List(f1),List(Pa)) val lkProof = Robinson2LK(resProof.get, seq) fixes issue 196 git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1217 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 19 September 2012, 13:23:37 UTC |
| ab68c1d | stefan.hetzl@gmail.com | 19 September 2012, 13:00:03 UTC | completed interpolation algorithm. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1216 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 19 September 2012, 13:00:03 UTC |
| d5b867e | cdunchev@gmail.com | 18 September 2012, 20:11:11 UTC | transformation of a grounded resolution term (resolution refutation) to a tree (LKProof with cuts and contractions only) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1215 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 September 2012, 20:11:11 UTC |
| 150fcad | giselle.mnr@gmail.com | 18 September 2012, 18:02:18 UTC | Created a new package called dssupport inside utils to put auxiliar methods on basic data structures (e.g. cartesian product of list or maps). Each data structure has its own scala file with the auxiliar functions. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1214 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 September 2012, 18:02:18 UTC |
| 02ddc15 | cdunchev@gmail.com | 18 September 2012, 15:11:57 UTC | Fixed issue 200 git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1213 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 September 2012, 15:11:57 UTC |
| 497c9c7 | shaolintl | 18 September 2012, 15:08:34 UTC | added the computation of projections as defined in Issue 196 git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1212 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 September 2012, 15:08:34 UTC |
| 1baa81b | cdunchev@gmail.com | 18 September 2012, 12:50:18 UTC | The resolution refutation is produced for the journal example after fixing the second-order substitution. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1211 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 September 2012, 12:50:18 UTC |
| 920af95 | cdunchev@gmail.com | 18 September 2012, 01:43:52 UTC | Very nice printing in Console for the struct. I also integrated it into ProofTool. The names of the proofs (greek symbols) are substituted by the correct symbols, i.e. \sigma by σ etc... git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1210 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 September 2012, 01:43:52 UTC |
| c057a91 | stefan.hetzl@gmail.com | 17 September 2012, 20:32:08 UTC | added preliminary version of interpolation algorithm fixing the interface. current functionality: extracts interpolants from proofs consisting of disjunction-left and disjunction-right inferences only. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1209 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 17 September 2012, 20:32:08 UTC |
| de85f1f | cdunchev@gmail.com | 17 September 2012, 18:50:54 UTC | Convenient feature ContinueAutoProp(seq: FSequent): Option[LKProof] has been added. This was requested by Issue 200 : "AutoProp should return None in case its input is not provable". git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1208 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 17 September 2012, 18:50:54 UTC |
| 7f751f9 | mrukhaia | 17 September 2012, 16:36:31 UTC | Unfolding of FO schematic proofs is integrated in ProofTool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1207 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 17 September 2012, 16:36:31 UTC |
