| 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 |
| abe86b3 | cdunchev@gmail.com | 27 August 2012, 22:13:09 UTC | Some of the propositional schemata examples were failing, so to keep the algorithms monotone, i.e. the new algorithms to work on the older examples, some type-casting has been done. An interesting question is why the BetaNormalization fails now, for example: // require( betaNormalize( App(Abs(v, f), ub) ) == auxf.formula ) fails as well as all requirements in slk.scala fail. The only change is that auxf.formula is not a SchemaFormula anymore, but a HOLFormula. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1171 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 August 2012, 22:13:09 UTC |
| 6f1e9be | cdunchev@gmail.com | 27 August 2012, 20:26:34 UTC | git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1170 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 August 2012, 20:26:34 UTC |
| 5fcbb0c | cdunchev@gmail.com | 27 August 2012, 20:18:39 UTC | The subtraction (minus 1) was extended to the first-order schemata. This was needed for getting the corresponding formula occurrences in the base case of a proof schema which is essential step for extracting the projection term for a given cut-configuration. As a sequence the projection term for the example in the journal paper is extracted correctly now. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1169 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 August 2012, 20:18:39 UTC |
| e1e6aa2 | cdunchev@gmail.com | 27 August 2012, 15:27:08 UTC | A nasty printing was commented out. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1168 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 August 2012, 15:27:08 UTC |
| 7a77412 | Martin.Riener | 27 August 2012, 15:09:14 UTC | removed post autopropositional transformations from the project, as it is now contained in shlk git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1167 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 August 2012, 15:09:14 UTC |
| e01593e | cdunchev@gmail.com | 27 August 2012, 15:05:56 UTC | A superfluous information has been removed from the extraction of the proj.term. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1166 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 August 2012, 15:05:56 UTC |
| 5c13d72 | mrukhaia@gmail.com | 26 August 2012, 20:12:27 UTC | Small typo is fixed in FOL schema parser. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1165 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 August 2012, 20:12:27 UTC |
| e3ad592 | cdunchev@gmail.com | 26 August 2012, 17:56:57 UTC | A bug in the matching has been fixed. The nice printing in Console is again OK. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1164 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 August 2012, 17:56:57 UTC |
| e4fefcd | cdunchev@gmail.com | 26 August 2012, 15:01:28 UTC | Projection term for first-order schema has been done. The relevant cut-configuration for the clause set have been started. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1163 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 August 2012, 15:01:28 UTC |
| 9c34518 | cdunchev@gmail.com | 25 August 2012, 13:25:21 UTC | The proof projections have been modified in order to capture the schematic first-order CERES. This change requiered some minor change in the following files. The projections for schematic first-order still do not work because of the skolemization. There was a problem which Martin found a few months ago. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1162 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 25 August 2012, 13:25:21 UTC |
| 5ae9149 | cdunchev@gmail.com | 24 August 2012, 14:19:32 UTC | The case for t.r.s. Rule has been added to the projections. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1161 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 24 August 2012, 14:19:32 UTC |
| cd83fde | mrukhaia | 23 August 2012, 14:58:19 UTC | indexed first-order variables are now printed in prooftool correctly. Also the journal example is completed (with autopropositional). git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1160 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 23 August 2012, 14:58:19 UTC |
| 570773d | cdunchev@gmail.com | 23 August 2012, 13:57:30 UTC | A journal example has been parsed. Autoprop works as well. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1159 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 23 August 2012, 13:57:30 UTC |
| 44c4e05 | cdunchev@gmail.com | 23 August 2012, 10:34:32 UTC | By mistake yesterday I commited a .iml file. Now I fix this mistake. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1158 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 23 August 2012, 10:34:32 UTC |
| 9c7f778 | cdunchev@gmail.com | 23 August 2012, 00:47:38 UTC | git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1157 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 23 August 2012, 00:47:38 UTC |
| a227c2b | cdunchev@gmail.com | 23 August 2012, 00:28:37 UTC | A normalization for the base case of the t.r.s. has been fixed (and tested) A substitution has been added (i.e. redundant) in the file schema.scala, because due ti the cycles of dependencies it was not visible. The parsing of first-order variable was made more precisely using the class foVar defined in schema.scala Example using indexed variables has been almost completed. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1156 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 23 August 2012, 00:28:37 UTC |
| 5eaa6bd | mrukhaia | 22 August 2012, 16:08:49 UTC | Some cosmetic improvements in prooftool. Also one more example file is added in integration tests git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1155 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 22 August 2012, 16:08:49 UTC |
| 7c24f98 | mrukhaia | 22 August 2012, 12:53:43 UTC | FOL parser for schemata is integrated in prooftool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1154 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 22 August 2012, 12:53:43 UTC |
| 13ef277 | cdunchev@gmail.com | 22 August 2012, 12:32:40 UTC | The arrow sign of the ArrowRule for nice printing in prooftoof has been added. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1153 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 22 August 2012, 12:32:40 UTC |
| 0a36f29 | cdunchev@gmail.com | 22 August 2012, 12:17:01 UTC | Auto-propositional has been added to the parser and successfully tested on the example from the journal paper git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1152 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 22 August 2012, 12:17:01 UTC |
| 7895d50 | shaolintl@gmail.com | 22 August 2012, 09:44:56 UTC | added a transformation from Robinson resolution calculus to LK. Can be called from CLI using Robinson2LK git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1151 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 22 August 2012, 09:44:56 UTC |
| 3f4b3a9 | cdunchev@gmail.com | 21 August 2012, 21:38:53 UTC | a missing cases in the cloning have been added. One of the base cases in the example has been completed. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1150 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 August 2012, 21:38:53 UTC |
| 3d41fa5 | cdunchev@gmail.com | 21 August 2012, 20:27:23 UTC | this is to make Jenkins again stable git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1149 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 August 2012, 20:27:23 UTC |
| cf5fd8f | cdunchev@gmail.com | 21 August 2012, 19:52:49 UTC | the example from the journal paper is unfolded for a given instance and the formulas/terms are normalized with respect to a t.r.s. which is parsed from the .lks input file. The arrow rule has been added. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1148 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 August 2012, 19:52:49 UTC |
| 287b935 | cdunchev@gmail.com | 21 August 2012, 11:23:02 UTC | this file was renamed and removed to shlk and to integration_tests. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1147 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 August 2012, 11:23:02 UTC |
| b786819 | cdunchev@gmail.com | 21 August 2012, 11:21:01 UTC | another renaming of files has been performed. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1146 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 August 2012, 11:21:01 UTC |
| 9f8821f | cdunchev@gmail.com | 21 August 2012, 11:08:31 UTC | a renaming which is more intuitive has been done git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1145 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 21 August 2012, 11:08:31 UTC |
| 858ec3f | shaolintl@gmail.com | 18 August 2012, 20:38:43 UTC | added sbt support for two nested module which makes compilation and testing much faster (due to incremental compilation) in order to use it one must install sbt and execute sbt from the appropriate module root directory. Some notes: - I am using an old sbt jar file (0.7.7) as I could not make the newest one (0.12.0) use the maven repository) - the target directories for classes and test-classes are the same as for maven - I did not find how to make a maven timestamp in the target folder so maven will recompile everything when creating the jar - the current workflow is therefore: - sbt is now installed per module and therefore cannot be called from a super module -- compile and test using sbt -- call maven install after finishing which will recompile everything git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1141 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 August 2012, 20:38:43 UTC |
| e8212e4 | cdunchev@gmail.com | 18 August 2012, 15:30:24 UTC | a test for testing autopropositional. A generator given me by Stefan is used. In the integration test can be visualised by prooftool. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1140 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 August 2012, 15:30:24 UTC |
| 73784e2 | cdunchev@gmail.com | 18 August 2012, 15:12:32 UTC | otimizing some imports git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1139 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 August 2012, 15:12:32 UTC |
| 2e6027a | cdunchev@gmail.com | 18 August 2012, 14:26:17 UTC | The last one from a series of optimizing imports. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1138 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 August 2012, 14:26:17 UTC |
| bfc410a | cdunchev@gmail.com | 18 August 2012, 11:45:07 UTC | the superflous imports have been removed git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1137 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 August 2012, 11:45:07 UTC |
| afa2b07 | cdunchev@gmail.com | 18 August 2012, 11:14:59 UTC | pointing to the corerct import git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1136 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 August 2012, 11:14:59 UTC |
| beffbd9 | cdunchev@gmail.com | 18 August 2012, 10:49:43 UTC | some refactoring git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1135 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 August 2012, 10:49:43 UTC |
| 602bca8 | cdunchev@gmail.com | 18 August 2012, 09:42:57 UTC | Some reorganization of the code has been performed. The reason to do is that I could not import projects to another projects due to cycles in the .pom This also why I had code duplications before. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1134 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 18 August 2012, 09:42:57 UTC |
| 2bffb9e | cdunchev@gmail.com | 17 August 2012, 11:06:28 UTC | Some improvements for autopropositional git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1133 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 17 August 2012, 11:06:28 UTC |
| 092157f | cdunchev@gmail.com | 16 August 2012, 19:10:41 UTC | commenting out 2 lines which make Jenkins unstable. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1132 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 16 August 2012, 19:10:41 UTC |
| 5ce9e51 | cdunchev@gmail.com | 16 August 2012, 18:29:43 UTC | some indeces have been adjusted. The unfolding of the example is ready. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1131 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 16 August 2012, 18:29:43 UTC |
| 4f7b01a | cdunchev@gmail.com | 16 August 2012, 18:26:55 UTC | The example from the journal paper. Later I will find a better name. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1130 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 16 August 2012, 18:26:55 UTC |
| 6d28f84 | cdunchev@gmail.com | 15 August 2012, 23:06:57 UTC | Small changes git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1129 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 August 2012, 23:06:57 UTC |
| 89c772a | cdunchev@gmail.com | 15 August 2012, 22:23:57 UTC | This will fix Jenkins git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1128 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 August 2012, 22:23:57 UTC |
| 4ad20b5 | cdunchev@gmail.com | 15 August 2012, 22:07:04 UTC | this will fix Jenkins :) git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1127 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 August 2012, 22:07:04 UTC |
| 5e7e3ea | cdunchev@gmail.com | 15 August 2012, 21:53:28 UTC | some small changes git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1126 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 August 2012, 21:53:28 UTC |
| da2d04e | cdunchev@gmail.com | 15 August 2012, 21:49:34 UTC | A few examples from FOL provided by Stefan have been tested successfully. This caused some failures to the schemata tests, but they are fixed so far. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1125 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 August 2012, 21:49:34 UTC |
| 5246368 | cdunchev@gmail.com | 15 August 2012, 13:37:01 UTC | The t.r.s is parsed git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1124 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 15 August 2012, 13:37:01 UTC |
| fd96f75 | cdunchev | 14 August 2012, 20:17:44 UTC | A missing case for the non-schematic sequent has been added. This is motivated by a discussion which I have with Stefan for the autoprop feature in iCERES. We are very close to fix this problem in general. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1122 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 14 August 2012, 20:17:44 UTC |
| f7ad7f6 | cdunchev@gmail.com | 13 August 2012, 11:22:08 UTC | Some data structures for first-order schemata have been added. The unfolding of a first-order schema proof was successfully tested with the term-rewriting system. Some rules have been changed in a way that the term-rewriting system is applied to the auxiliary formulas, i.e. modulo t.r.s. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1121 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 13 August 2012, 11:22:08 UTC |
| 772ff73 | stefan.hetzl@gmail.com | 27 July 2012, 18:42:08 UTC | enhancements to CLI - moved AutoProp to top-level git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1120 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 27 July 2012, 18:42:08 UTC |
| 8872430 | cdunchev@gmail.com | 26 July 2012, 11:02:46 UTC | Exclude one of the redundant files for autoProp. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1119 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 26 July 2012, 11:02:46 UTC |
| 54cb901 | cdunchev@gmail.com | 25 July 2012, 11:21:14 UTC | The same problem as in the prevoius commit has been fixed. P.S. The code should be splitted at some point. git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1118 85d21ef8-add0-11de-ae77-5bfb9c5a3f34 | 25 July 2012, 11:21:14 UTC |
