nti

https://github.com/etiennepayet/nti

Science Score: 36.0%

This score indicates how likely this project is to be science-related based on various indicators:

○
CITATION.cff file
✓
codemeta.json file
Found codemeta.json file
✓
.zenodo.json file
Found .zenodo.json file
○
DOI references
✓
Academic publication links
Links to: arxiv.org
○
Academic email domains
○
Institutional organization owner
○
JOSS paper metadata
○
Scientific vocabulary similarity
Low similarity (9.3%) to scientific vocabulary

Last synced: 10 months ago · JSON representation

Repository

Basic Info

Host: GitHub
Owner: etiennepayet
License: gpl-3.0
Language: Java
Default Branch: master
Size: 10.1 MB

Statistics

Stars: 1
Watchers: 1
Forks: 0
Open Issues: 0
Releases: 0

Created over 3 years ago · Last pushed 11 months ago

Metadata Files

Readme License Authors Codemeta

README.md

NTI is a free software distributed under the terms of the GNU Lesser General Public License, version 3 or any later version. It is developed and maintained by Étienne Payet.

Usage: java -jar nti.jar <file> [action] [options]

NTI tries to prove (non)termination of the program in the provided file. - For logic programs, the implemented techniques are described in [Payet & Mesnard, TOPLAS'06] and [Payet, TPLP'25]. - For TRSs, the implemented technique uses the dependency pair (DP) framework: first, it decomposes the initial set of DP problems into subproblems using sound DP processors, then it tries to prove that the unsolved subproblems are infinite using the approaches of [Payet, TCS'08], [Payet, LOPSTR'18] and [Payet, JAR'24].

file has to conform to the TPDB syntax specification (see here and here). It has one of the following suffixes: - .pl for a pure logic program - .ari for a TRS or an SRS in the ARI format - .xml for a TRS or an SRS in the old XML format - .trs for a TRS in the old, human readable, format - .srs for an SRS in the old, human readable, format

action (optional) can be: - -h|--help: print this help - --version: print the version of NTI - -print: print the program in the given file - -stat: print some statistics about the program in the given file - -prove: run a (non)termination proof of the program in the given file (THIS IS THE DEFAULT ACTION)

options (optional) can be: - -v: verbose mode (for printing proof details in the final output) - -t=n: set a time bound on the nontermination proofs (n is the time bound in seconds) - -cTI=path: set the path to cTI (for proving termination of logic programs)
If no path to cTI is set, then only nontermination proofs are run for logic programs

Owner

Login: etiennepayet
Kind: user

Repositories: 3
Profile: https://github.com/etiennepayet

CodeMeta (codemeta.json)

{
  "@context": "https://doi.org/10.5063/schema/codemeta-2.0",
  "@type": "SoftwareSourceCode",
  "license": "https://spdx.org/licenses/LGPL-3.0+",
  "codeRepository": "https://github.com/etiennepayet/nti",
  "dateCreated": "2007-05-21",
  "datePublished": "2007-05-21",
  "dateModified": "2023-11-13",
  "name": "NTI",
  "description": "NTI is a non-termination prover for term-rewriting systems and logic programs.",
  "applicationCategory": "Computer Science",
  "developmentStatus": "active",
  "funder": {
    "@type": "Organization",
    "name": "Universit de La Runion"
  },
  "keywords": [
    "Non-Termination",
    "Term Rewriting",
    "Logic Programming"
  ],
  "programmingLanguage": [
    "Java 8"
  ],
  "runtimePlatform": [
    "JVM"
  ],
  "author": [
    {
      "@type": "Person",
      "@id": "https://orcid.org/0000-0002-3519-025X",
      "givenName": "tienne",
      "familyName": "Payet",
      "email": "etienne.payet@univ-reunion.fr",
      "affiliation": {
        "@type": "Organization",
        "name": "LIM, Universit de La Runion, France"
      }
    }
  ]
}

ecosyste.ms

Data

Tools

Indexes

Applications

Experiments

Open Source Science

nti