Benutzer-Werkzeuge

Webseiten-Werkzeuge


dokumentation:changelog

ChangeLog of the Naproche System

Version 0.47 -- 8. June 2010 -- Revision 600

Linguistic Module
  • Prepositional phrases, including prepositions with collective predicates like „between“
Developers
  • Marcos Cramer

Version 0.46 -- 25. March 2010 -- Revision 590

General
  • Several minor Bugfixes
Website
  • Added warning messages (orange color) when a contradiction was derived from the axioms of an obligation. However, no warning is displayed when the obligation is part of a proof by contradiction. Total number of warnings is displayed at the end.
Linguistic Module
  • Treatment of quantifiers in biconditionals an reversed conditionals improved.
  • Changed and improved handling of plurals.
  • Improved warning messages.
Logic Module
  • „The“ conditions are now properly skolemized.
  • If an obligation fails, there is now one last try with all available premises.
  • Support for plural conditions added.
  • Changed premise selection to make smaller steps. Therefore, the discharge process takes longer.
  • see Website.
Developers
  • Marcos Cramer
  • Daniel Kühlwein
  • Richard Schüller

Version 0.45 -- 7. Dezember 2009 -- Revision 506

General
  • Further improved output.
  • Implemented debug/normal user modes.
Website
  • Graphic improvements of the LaTeX menu.
  • The LaTeX support now uses Kile icons. This should make future extensions easy.
Linguistic Module
  • „the“ constructions are now supported.
Logic Module
  • „the“ conditions are now supported.
Development Utils
  • display_tree and display_tree_list create SVG graphs from GULP lists.
Developers
  • Marcos Cramer
  • Daniel Kühlwein
  • Sebastian Zittermann

Version 0.41 -- 1. November 2009

General
  • Moved Preparsing from Prolog to Website. It is now done in PHP.
  • Changed error message output.
  • Changed server from HIM to Duisburg-Essen.
  • Prolog Documentation Server is working again.
Website
  • Preparse output can now be copy-pasted into Prolog.
  • Statistics are displayed.
  • Parse errors can now be clicked to focus the textarea to the word which could not be parsed.
Linguistic Module
  • Sub-PRSs for conjuncts.
  • Differentiate conjuncts which proceed with the argument („and therefore …“) from normal conjuncts.
  • References which are only attached to subclauses.
Logic Module
  • Improved create_obligations algorithm speed dramatically (no more assert/retract).
  • Premise selection algorithm implemented.
  • Obligation graph has been changed. It now links all new premises (= premises that were not available in the last obligation) to the conjecture.
  • Changed create_obligations algorithm:
    • Implications are treated like assumption if CheckTrigger=Check.
    • Conjuncted holds Formulas are split. A seperate obligation is created for each subformula.
Developers
  • Marcos Cramer
  • Daniel Kühlwein
  • Sebastian Zittermann

Version 0.4 -- 1. October 2009

  • Linguistic module:
    • Plurals and NP coordination.
    • Improved PRS creation algorithm speed dramatically (more cuts).
  • Added Proof Graphs.
  • Changed the graphical layout of the website.
  • Added PDF creation option on the website.
Developers
  • Marcos Cramer
  • Daniel Kühlwein
  • Sebastian Zittermann

Version 0.3 -- June 2009

  • Introduced web interface
  • Linguistic module:
    • Much more linguistic constructions now possible: Nouns, verbs, adjectives, such-that-clauses etc.
    • Completely rewrote the PRS creation algorithm.
  • Logic module: Adaptions to new PRS conditions.
Developers
  • Marcos Cramer
  • Daniel Kühlwein
  • Mona Rahn
  • John Schmid

Version 0.2 -- July 2008

  • Linguistic module: Introduced PRSs (Proof Representation Structures).
  • Logic module: Checking PRSs for correctness by using external prover and TPTP software.
Developers
  • Doerthe Arndt
  • Merlin Carl
  • Shruti Gupta
  • Nickolay Kolev
  • Daniel Kühlwein
  • Bhoomija Ranjan

Version 0.1 -- 2007

  • Interface: Texmacs Plugin
  • Linguistic module:
    • Direct translation of single sentences into first order logic.
    • Sentences consist of formulas, natural language connectives, natural language quantifiers and proof structure triggers like „assume“ and „thus“.
  • Logic module: Home-made prover
Developers
  • Peter Koepke
dokumentation/changelog.txt · Zuletzt geändert: 2010/06/16 15:00 von mcr