Nothing Special   »   [go: up one dir, main page]

Reger, 2016 - Google Patents

Better Proof Output for Vampire.

Reger, 2016

View PDF
Document ID
18352371083826508605
Author
Reger G
Publication year
Publication venue
Vampire@ IJCAR

External Links

Snippet

Vampire produces highly usable and informative proofs, but now they are even better and this paper explains how. It is important that the proofs produced by automated theorem provers are both understandable and machine checkable. Producing something that …
Continue reading at easychair.org (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/20—Handling natural language data
    • G06F17/21—Text processing
    • G06F17/22—Manipulating or registering by use of codes, e.g. in sequence of text characters
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • G06F17/30286—Information retrieval; Database structures therefor; File system structures therefor in structured data stores
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/20—Handling natural language data
    • G06F17/27—Automatic analysis, e.g. parsing
    • G06F17/2705—Parsing
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • G06F17/30943—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type
    • G06F17/30946—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type indexing structures
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/30—Creation or generation of source code
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/70—Software maintenance or management
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/02—Knowledge representation
    • G06N5/022—Knowledge engineering, knowledge acquisition
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06Q—DATA PROCESSING SYSTEMS OR METHODS, SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q10/00—Administration; Management

Similar Documents

Publication Publication Date Title
Sun et al. Formal semantics and verification for feature modeling
Mauro et al. Context aware reconfiguration in software product lines
Bønneland et al. Simplification of CTL formulae for efficient model checking of Petri nets
Wardhana et al. Transformation of sysml requirement diagram into owl ontologies
Leblebici et al. Leveraging incremental pattern matching techniques for model synchronisation
Reger Better Proof Output for Vampire.
Pease et al. Knowledge engineering for large ontologies with Sigma KEE 3.0
Aït-Ameur et al. Empowering the event-b method using external theories
Konnov et al. Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
AU2016201776A1 (en) Functional use-case generation
Leonard et al. Program synthesis from formal requirements specifications using APTS
Jongeling et al. Lightweight Consistency Checking for Agile Model-Based Development in Practice.
Osama et al. Srcm: A semi formal requirements representation model enabling system visualisation and quality checking
Mäder et al. Ready-to-use traceability on evolving projects
Curland et al. Enhanced verbalization of ORM models
Vu et al. Faithfully formalizing OSEK/VDX operating system specification
Zhu et al. A supporting tool for syntactic analysis of SOFL formal specifications and automatic generation of functional scenarios
Ipate et al. Model learning and test generation using cover automata
Benzmüller et al. Progress report on LEO-II, an automatic theorem prover for higher-order logic
Singh et al. Stateflow to tabular expressions
Abdelmalek et al. A Bimodal Approach for the Discovery of a View of the Implementation Platform of Legacy Object-Oriented Systems under Modernization Process.
Guerrero et al. Smart Design of Similarity Relations for Fuzzy Logic Programming Environments
Curland et al. A role calculus for ORM
CN116069669B (en) Full-automatic distributed consistency analysis method, system, equipment and storage medium
Madeira et al. When even the interface evolves...