7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7f |
|
22-Aug-2017 |
Eugen Kuksa <kuksa.eugen@gmail.com> |
Complete TPTP support (#1707)
* Add option to print the AST in XML/JSON output. Turn it off by default.
* Add abstract syntax of TPTP.
* Add parens and brackets to Common.Lexer.
* Add TPTP Parser.
* Add TPTP Sign.
* Add TPTP Morphism.
* Add TPTP StaticAnalysis.
* Fix IRI character parsing.
* Add TPTP Pretty.
* Add TPTP Logic.
* Map the tptp and p file extension to the TPTP logic for input.
* Add LibDefn parser for TPTP.
* Write TPTP output.
* Add EProver to TPTP.
* Add TPTP Sublogics.
* Add SPASS prover to TPTP.
* Add Vampire prover to TPTP.
* Add Darwin prover to TPTP.
* Add Leo-II prover to TPTP.
* Add Geo-III prover to TPTP - It does not support a timeout.
* Add CVC4 prover to TPTP.
* Add Isabelle prover to TPTP.
* Make IRI compatible with TPTP library file names.
* Revert "fail if names of sentences appear as names of symbols #1630"
This is a combination of 3 commits:
* Revert "check that the Result has no errors"
This reverts commit 9542b929f3cfabf1491c3f0489acf92ba703968f.
* Revert "better error message"
This reverts commit a7ea46d4c76b11735234092d0a50efcbc56f9642.
* Revert "fail if names of sentences appear as names of symbols"
This reverts commit 2487bae09bf3aabc7085880aee616648fe5ca241.
* Fix usage of magic file
There were other (system) magic files invoked as well with a higher
priority. Using the MAGIC environment variable instead of the
argument --magic-file overrides this behaviour and only uses the
specified magic file.
* Fix magic file
The escaping of "@" and "(" is not needed.
The escaping of a trailing space in clif is needed.
* Add TPTP to magic file.
* Add Satallax prover to TPTP.
* Properly check for http[s] URIs.
* Allow file:// in libdirs.
* Allow only one http[s] libdir - Parse the port correctly.
* Fix all remaining parsing problems.
* Move functions to debug the parser to a separate module.
* Get rid of all TPTP related compiler warnings.
* Move the type 'Morphism' to 'TPTP.Morphism'.
* Rename: TPTP/Logic.hs -> TPTP/Logic_TPTP.hs
* Implement all_sublogics.
* Recognise negated_conjecture as a proof obligation. |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168 |
|
25-Mar-2016 |
Jens Elkner <jel+git@iws.cs.uni-magdeburg.de> |
applied utils/replaceAllHeaders.sh
- all $Header$ tokens in doc comments replaced with corresponding filename |
731b0689c37481ff271c1cedddd76b941c32de05 |
|
28-Jun-2013 |
Christian Maeder <Christian.Maeder@dfki.de> |
made it compile with ghc-6.12.3
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18028 cec4b9c1-7d33-0410-9eda-942365e851bb |
05fa51cf4404b1b8013522026a4f4597cf2f560f |
|
10-May-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
cleanup
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17957 cec4b9c1-7d33-0410-9eda-942365e851bb |
98890889ffb2e8f6f722b00e265a211f13b5a861 |
|
01-Sep-2010 |
Corneliu-Claudiu Prodescu <Corneliu-Claudiu.Prodescu@dfki.de> |
Added see license.txt to license field
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13959 cec4b9c1-7d33-0410-9eda-942365e851bb |
b87efd3db0d2dc41615ea28669faf80fc1b48d56 |
|
11-Aug-2010 |
Corneliu-Claudiu Prodescu <Corneliu-Claudiu.Prodescu@dfki.de> |
Changed haddock headers and inserted empty headers for the ones missing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13857 cec4b9c1-7d33-0410-9eda-942365e851bb |
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708 |
|
10-Mar-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed semicolons
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13197 cec4b9c1-7d33-0410-9eda-942365e851bb |
10b02b2343246df6773585636fe3ddbefa3b6a1b |
|
04-Mar-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored parsers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13160 cec4b9c1-7d33-0410-9eda-942365e851bb |
e64aab3e57d843884cd489cc3aa130120a400b05 |
|
26-Feb-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
used optionL parser
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13123 cec4b9c1-7d33-0410-9eda-942365e851bb |
97279257021fd703f25019ae8869d86f455d1ea1 |
|
26-Oct-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
hlinted
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12725 cec4b9c1-7d33-0410-9eda-942365e851bb |
bc625f556c977707b60ad57fd3f978ee03bc930c |
|
14-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed examples from code
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10322 cec4b9c1-7d33-0410-9eda-942365e851bb |
c2f6729d0a023361c459099eac25bb20f6c37d05 |
|
17-Apr-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
only allowed symbols in literals
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9933 cec4b9c1-7d33-0410-9eda-942365e851bb |
56207d3d8820aef00cba6d90139265a9bc7f9c3d |
|
17-Apr-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed separate simple terms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9930 cec4b9c1-7d33-0410-9eda-942365e851bb |
37c4e519e6f5f187d22fabe348808704ccffd505 |
|
01-Apr-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed problem identifier back to String
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9854 cec4b9c1-7d33-0410-9eda-942365e851bb |
bfe34c9d0a279f8f86eae778b761f32e4788d42d |
|
01-Apr-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed SPIdentifier to Token
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9853 cec4b9c1-7d33-0410-9eda-942365e851bb |
3e8a2f62e5b1a188c86b81173529750884faa18e |
|
12-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
improved SPSetting treatment
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8843 cec4b9c1-7d33-0410-9eda-942365e851bb |
c9c6b1015c802c215bc791350301d89b2bde4142 |
|
12-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused function
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8842 cec4b9c1-7d33-0410-9eda-942365e851bb |
25cac686bcbaa116c85d2bb618e709069ab10038 |
|
12-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
further refactored clauses
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8841 cec4b9c1-7d33-0410-9eda-942365e851bb |
dd18739ce1c4216190c66d3cd5d4cd8394292e73 |
|
12-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored SPLiteral
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8838 cec4b9c1-7d33-0410-9eda-942365e851bb |
f1bd301aff1cdffba15e9ffeed3f70f61b28c339 |
|
07-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
more corrections
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8807 cec4b9c1-7d33-0410-9eda-942365e851bb |
842ad298a9666f6de51ec53fabd6a9305b2bf245 |
|
04-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
identifiers may start with digits
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8789 cec4b9c1-7d33-0410-9eda-942365e851bb |
1f7e8d72a6636ba854cb9ab1f96353adc11e5ce9 |
|
04-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
tested clauses and proof steps
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8786 cec4b9c1-7d33-0410-9eda-942365e851bb |
887844c9d0c162630eba716c8ecb8f944cda2116 |
|
03-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
checked against TPTP Version 3.1.0
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8783 cec4b9c1-7d33-0410-9eda-942365e851bb |
f2e3a08e1f838140e2c533d22e178837934a230d |
|
03-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
parser is able to reparse Basic/*.dfg files
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8782 cec4b9c1-7d33-0410-9eda-942365e851bb |
5366c0cd087ad4ce1aeeb0a6addf77d290714d28 |
|
03-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
further refactored
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8781 cec4b9c1-7d33-0410-9eda-942365e851bb |
5406cee84d82bc23181c913eb1fe901303ae5b61 |
|
31-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored the whole
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8775 cec4b9c1-7d33-0410-9eda-942365e851bb |
e886f76655ea805ae1410610cddce301f930b87a |
|
13-Aug-2007 |
Heng Jiang <jiang@tzi.de> |
add Prover of Darwin;
SPASS-Parser (DFG-Parser) extended with SPASS-INPUT-SYNTAX v3.0
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8592 cec4b9c1-7d33-0410-9eda-942365e851bb |
89e9687ab1427723e373996ddb9686f68f5c21ba |
|
16-Jul-2007 |
Heng Jiang <jiang@tzi.de> |
modified the syntax of spass-input with version 1.5; added parser of clauseFormulaRelation, prooflist and settinglist into dfg-parser.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8376 cec4b9c1-7d33-0410-9eda-942365e851bb |
f04e8f3ff56405901be968fd4c6e9769239f1a9b |
|
26-Jun-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Renamed almost all files with SPASS into SoftFOL.
Only SoftFOL/Logic_SPASS remains.
It will be updated very soon.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8150 cec4b9c1-7d33-0410-9eda-942365e851bb |