| 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 |
| 2ffaf81 | cdunchev@gmail.com | 17 September 2012, 13:02:34 UTC | The new feature of unfolding is completed. Now it can be integrated also in prooftool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1206 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 17 September 2012, 13:02:34 UTC |
| d611a69 | cdunchev@gmail.com | 17 September 2012, 03:17:05 UTC | git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1205 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 17 September 2012, 03:17:05 UTC |
| c56c2d6 | cdunchev@gmail.com | 17 September 2012, 03:09:23 UTC | The unfolding was optimized. The intermediate step with the rewriting rules was skipped. The rewriting starts at the same time with the unfolding/instantiating. The jounal_example also works now. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1204 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 17 September 2012, 03:09:23 UTC |
| 7c59a16 | cdunchev@gmail.com | 16 September 2012, 11:24:14 UTC | I forgot to add the .slk file before I do a commit. I apologize. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1203 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 16 September 2012, 11:24:14 UTC |
| 25c33a6 | cdunchev@gmail.com | 15 September 2012, 22:04:15 UTC | git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1202 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 September 2012, 22:04:15 UTC |
| 438ed81 | cdunchev@gmail.com | 15 September 2012, 21:34:06 UTC | 1)The unfolded LK proof with ↠ rules has been transformed to an LK proof without ↠ rules, i.e. all the term-rewriting takes place in the axioms. Now we can extract the clause set with the usual CERES method. 2)some functionality for the resolution schema has been added. Soon I will improve it. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1201 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 September 2012, 21:34:06 UTC |
| e8f2d34 | cdunchev@gmail.com | 15 September 2012, 02:40:02 UTC | The resolution schemata is 99% ready. NB: The program even showed that the resolution refutation (ρ, \cal R) in example 6.8 from the journal paper is NOT correct. The given substitution θ = {x ← λk.h(k,x)} does not work because the formulas P(σ'(Sk)) and P(σ(Sk,x,SK)) never unify according to the rewriting rules for σ and σ' given in example 6.5 git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1200 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 September 2012, 02:40:02 UTC |
| 8f0b535 | mrukhaia@gmail.com | 14 September 2012, 15:05:04 UTC | Display view for Expansion Tree is refined. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1199 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 14 September 2012, 15:05:04 UTC |
| 45b95fc | mrukhaia | 13 September 2012, 16:21:31 UTC | Export of several proofs in tex (useful for proof schemata) is implemented. Also skeleton to display expansion trees is started. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1198 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 13 September 2012, 16:21:31 UTC |
| 5fa7f4c | cdunchev@gmail.com | 13 September 2012, 14:47:39 UTC | a resolution term and a resolution deduction are already implemented and successfully tested git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1197 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 13 September 2012, 14:47:39 UTC |
| ba394ba | mrukhaia | 12 September 2012, 18:59:00 UTC | Double click with right button on formulas popup a latex representation of it, which can be copied. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1196 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 12 September 2012, 18:59:00 UTC |
| 7c121af | mrukhaia | 11 September 2012, 15:40:28 UTC | Latex exporting is improved. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1195 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 11 September 2012, 15:40:28 UTC |
| f379fc2 | mrukhaia | 10 September 2012, 17:36:45 UTC | Scrolling works now also with mouse wheel. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1194 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 10 September 2012, 17:36:45 UTC |
| a5e0fcd | shaolintl | 10 September 2012, 11:27:28 UTC | - moved Clause and ResolutionProof to base from robinson package - moved Robinson2LK from transformations to algorithms git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1193 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 10 September 2012, 11:27:28 UTC |
| 53dd79d | cdunchev@gmail.com | 10 September 2012, 02:05:49 UTC | Integrating the substitution of the clause variable. Rewriting the clause-set schema to a clause-set schema term. Transforming the clause-set term to a set. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1192 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 10 September 2012, 02:05:49 UTC |
| 688ea83 | mrukhaia@gmail.com | 09 September 2012, 21:00:57 UTC | Some println-es and useless code are removed. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1191 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 09 September 2012, 21:00:57 UTC |
| 63c2ca3 | cdunchev@gmail.com | 09 September 2012, 15:45:47 UTC | The relevant characteristic clause set is extracted now. Joint work with Mikheil. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1190 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 09 September 2012, 15:45:47 UTC |
| bead79b | cdunchev@gmail.com | 09 September 2012, 03:06:46 UTC | The implementation for the Resolution proof schemata has been started. The Ex. 6.8 from the journal paper is the running example and it will be finished soon. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1189 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 09 September 2012, 03:06:46 UTC |
| aeeefb8 | cdunchev@gmail.com | 08 September 2012, 13:27:47 UTC | Two new tests for quiantified formulas have been added in addition to the tests in NNFTest.scala from r1187. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1188 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 September 2012, 13:27:47 UTC |
| ae575e8 | fraini | 08 September 2012, 07:51:25 UTC | Renamed NNF tests. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1187 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 September 2012, 07:51:25 UTC |
| 0f26deb | cdunchev@gmail.com | 08 September 2012, 02:03:42 UTC | The unfolding of a ground schema clause term has been implemented. (Example 6.5 from the journal paper) The unfolding is with respect to the arithmetical variables only. For the case of clause variables and schema clause term variables will be ready soon. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1186 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 08 September 2012, 02:03:42 UTC |
| 8d8c56f | cdunchev@gmail.com | 07 September 2012, 21:20:49 UTC | A test file for the Negation Normal Form. P.S. As a gift for my friend Tomer :) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1185 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 07 September 2012, 21:20:49 UTC |
| a262535 | mrukhaia | 07 September 2012, 15:36:51 UTC | LaTeX export is refined and added in context menu to export a subproof. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1184 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 07 September 2012, 15:36:51 UTC |
| 6d2b0d4 | shaolintl@gmail.com | 07 September 2012, 13:09:16 UTC | moved the NNF transformation from ceres to algorithms. We have some problem with names of modules which we should clarify. I think transformations should contain only programs for transformations and things like NNF be placed under algorithms. Anyway, it should not be in CERes as it can be used by other programs. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1183 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 07 September 2012, 13:09:16 UTC |
| bba132c | mrukhaia@gmail.com | 06 September 2012, 22:18:59 UTC | Now Prooftool can export proof in latex. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1182 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 06 September 2012, 22:18:59 UTC |
| 90a115f | cdunchev@gmail.com | 06 September 2012, 01:42:00 UTC | Clause schema term has been implemented. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1181 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 06 September 2012, 01:42:00 UTC |
| 2d7e51e | cdunchev@gmail.com | 04 September 2012, 02:10:43 UTC | Clause schemata has been tested successfully on the example 6.1 from the journal paper. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1180 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 04 September 2012, 02:10:43 UTC |
| fd8e598 | cdunchev@gmail.com | 03 September 2012, 02:15:34 UTC | Small step for clause schemata, giant leap for resolution schemata. :) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1179 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 03 September 2012, 02:15:34 UTC |
| d1ea576 | cdunchev@gmail.com | 02 September 2012, 18:23:58 UTC | The nice printing in console has been improved including the case for the sTerm git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1178 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 02 September 2012, 18:23:58 UTC |
| f3ee4e7 | cdunchev@gmail.com | 02 September 2012, 17:44:55 UTC | the console printing of the exptype of a lambdaTerm has been improved. For example, instead "ind" now is printed "ω" for the indexed expressions. Instead of "i" now is printed "ι". git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1177 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 02 September 2012, 17:44:55 UTC |
| d569621 | cdunchev@gmail.com | 30 August 2012, 01:36:48 UTC | continue implementation of the clause schemata. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1176 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 30 August 2012, 01:36:48 UTC |
| 963d879 | mrukhaia | 28 August 2012, 16:11:09 UTC | Error messages are better displayed now. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1175 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 August 2012, 16:11:09 UTC |
| 966aa61 | giselle.mnr@gmail.com | 28 August 2012, 15:20:57 UTC | Added information to the user's manual and organized more the ceresHelp string. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1174 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 August 2012, 15:20:57 UTC |
| d2a6cad | Martin.Riener | 28 August 2012, 13:20:35 UTC | regularization now adds curly brackets around the indices of fresh variants of given variables git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1173 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 August 2012, 13:20:35 UTC |
| 0857aa2 | mrukhaia | 28 August 2012, 12:50:38 UTC | Added export to pdf files. Also some improvements of the code like removed outdated test examples and constraints (minimal and maximal values of fonts) for zooming changed. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1172 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 28 August 2012, 12:50:38 UTC |
