GitHub PushEvent at 2014-10-08 08:28:52
Repository: gapt
Actor: gebner
Payload: {"shas":[["d14da0b2fd8992e32161c920068ddba9b4987d92","14b411be59ed7ad577cfffa4d65d71b140dee865@gmail.com","Cleaned up and reorganized some code as per Stefan's suggestions.\n\n\ngit-svn-id: http://gapt.googlecode.com/svn/trunk@2164 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","szivota@gmail.com",true],["a91a708cd57746a45dbd1a16a068da10aa61e3a9","14b411be59ed7ad577cfffa4d65d71b140dee865@gmail.com","Added an algorithm that converts MultiExpansionTrees to ExpansionTrees, along with a simple unit test. Consequently, minimalExpansionSequents can now be applied to ExpansionSequents by converting back and forth.\n\n\ngit-svn-id: http://gapt.googlecode.com/svn/trunk@2165 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","szivota@gmail.com",true],["2e0a6da058693d21188f9a98fb89094b73c34973","e638ab3837677cf8b817a2bb04da8e9aa74967e9@85d21ef8-add0-11de-ae77-5bfb9c5a3f34","ral: fixed atomic factor rules, paramodulation allows flipped equiations too now \n\ngit-svn-id: http://gapt.googlecode.com/svn/trunk@2166 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","Martin.Riener",true],["519cca440b6eb83237df5f8ffe0eebd71d89bf5b","e638ab3837677cf8b817a2bb04da8e9aa74967e9@85d21ef8-add0-11de-ae77-5bfb9c5a3f34","started with ceres omega\n\ngit-svn-id: http://gapt.googlecode.com/svn/trunk@2167 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","Martin.Riener",true],["d04ecaabc0f9a4f084a1eb8ed88a6ec650aec59e","e638ab3837677cf8b817a2bb04da8e9aa74967e9@85d21ef8-add0-11de-ae77-5bfb9c5a3f34","prover9 import: flips on negative literals were not correctly translated. the solution implemented atm adds a tautological clause t=s :- t=s to the clause set to do the translation (see comments in the code for the full inference). this is a bit ugly, do you know anything better? fixes issue 268.\n\ngit-svn-id: http://gapt.googlecode.com/svn/trunk@2168 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","Martin.Riener",true],["ea3451c0a1d6eff55e6bd513a19362b122618215","14b411be59ed7ad577cfffa4d65d71b140dee865@gmail.com","Restructured and improved the minimalExpansionSequents algorithm. It should now be able to handle expansion trees of arbitrary structure. I also generalized my list helper functions to sequences.\n\n\ngit-svn-id: http://gapt.googlecode.com/svn/trunk@2169 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","szivota@gmail.com",true],["7ada297e9ff45e7be51a828ee7678b75eccb58e3","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Adding a better structured and uniform directory for TSTP proofs.\n\ngit-svn-id: http://gapt.googlecode.com/svn/trunk@2170 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",true],["b345fffe2d753a05688bb51d628a6d2c0ffde782","edfb45cab452b4b9d5f17986a4b9f29c2e85ea4e@gmail.com","TreeGrammarDecomposition: Major bug fixes for instances with n>=2 (i.e. for introducing more than 1 cut). \nNot only the sufficient set of keys was not generated the right way, but also the MinCostSAT formulation was faulty.\nEverything fixed and should now work out just fine.\nMaxSAT: switched a debug to a trace call, since it is not usually necessary\n\ngit-svn-id: http://gapt.googlecode.com/svn/trunk@2171 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","christoph.spoerk@gmail.com",true],["f3dc8f6e81c51c3111d6032b75c3fb80028a1c1e","2ee8ec943467fad83db2eb3f247bb99e61ef3d05@gebner.org","Merge remote-tracking branch 'svn/trunk'","Gabriel Ebner",true]],"size":9,"ref":"refs/heads/master","head":"f3dc8f6e81c51c3111d6032b75c3fb80028a1c1e"}