Automating the synthesis of decision procedures in a constructive metatheory

DOI10.1023/A:1018943603394MaRDI QIDQ1267772zbMATH OpenOpenAlexFDO

Authors Alessandro Armando, Jason Gallagher, Alan Smaill, Alan Bundy

Publication date 25 November 1998

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1018943603394

zbMATH Keywords

decision proceduresproof-planningpropositional logic

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Mechanizing metatheory in a logical framework
• Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic
• Publication:4503902
• Advances in Artificial Intelligence
• Automated reasoning with a constraint-based metainterpreter
• scientific article; zbMATH DE number 4155932
• Automating automated reasoning. The case of two generic automated reasoning tools
• Mechanizing Mathematical Reasoning

Cited in

(4)

• scientific article; zbMATH DE number 2177631 (Why is no real title available?)
• scientific article; zbMATH DE number 1863392 (Why is no real title available?)
• Learning strategies for mechanised building of decision procedures
• Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic

Describes a project that uses

Uses Software

• Nuprl
• CLAM

This page was built for publication: Automating the synthesis of decision procedures in a constructive metatheory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1267772)